机读格式显示(MARC)

• 000 01402cam 2200373 a 4500

• 000 1000077919

• 001 0000301785

• 005 20051231091201.0

• 008 020312s2002 gw a b 001 0 eng

• 010 __ |a 2002020906

• 020 __ |a 3540433767 (softcover : alk. paper) : |c CNY200.00

• 040 __ |a DLC |c DLC |d C$Q |d OHX |d SCT

• 050 00 |a QA76.9.L63 |b I83 2002

• 082 00 |a 004.01/5113 |2 21

• 090 __ |a TP301.6/NT

• 093 __ |a TP301.6 |2 4

• 099 __ |a CAL 022002177008

• 100 1_ |a Nipkow, Tobias, |d 1958-

• 245 10 |a Isabelle/HOL : |b a proof assistant for higher-order logic / |c Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel.

• 260 __ |a Berlin ; |a New York : |b Springer, |c c2002.

• 300 __ |a xiii, 218 p. : |b ill. ; |c 24 cm.

• 490 1_ |a Lecture notes in computer science, |x 0302-9743 ; |v 2283. |a Tutorial

• 504 __ |a Includes bibliographical references (p. [209]-211) and index.

• 530 __ |a Also available via the World Wide Web.

• 650 _0 |a Computer logic.

• 650 _0 |a Automatic theorem proving.

• 700 1_ |a Paulson, Lawrence C.

• 700 1_ |a Wenzel, Markus.

• 830 _0 |a Lecture notes in computer science ; |v 2283.

• 830 _0 |a Lecture notes in computer science. |p Tutorial.

• 901 __022005000735

• 905 __ |a CAU |f TP301.6/NT |b W0074882(or.)

• 907 __ |a CAU |f TP301.6/NT |b W0074882(or.)

• 999 __ |t C |A xy1 |a 20051230 11:23:01 |I xy1 |i 20051231 09:12:01 |G wzhlc |g 20060307 15:53:3