599

1 
$Id$


2 
ERRATA in the book "Isabelle: A Generic Theorem Prover"


3 
by Lawrence C. Paulson (contributions by Tobias Nipkow)


4 


5 
Some of these errors are typographical but most of them are due to continuing


6 
changes to Isabelle.

456

7 

491

8 
Thanks to Sara Kalvala, Tobias Nipkow


9 

599

10 


11 
INTRODUCTION TO ISABELLE


12 


13 
Advanced Methods


14 

1083

15 
page 46: the theory sections can appear in any order


16 


17 
page 48: theories may now contain a separate definition part


18 

599

19 
page 52, middle: the declaration "types bool,nat" should be "types bool nat"

456

20 

599

21 
page 57, bottom: should be addsimps in


22 
val add_ss = FOL_ss addrews [add_0, add_Suc]


23 


24 


25 
ISABELLE REFERENCE MANUAL

456

26 

599

27 
Introduction


28 


29 
page 67: show_brackets is another flag, controlling display of bracketting


30 


31 
Tactics

456

32 

599

33 
page 85: subgoals_tac is another tactic, for multiple calls to subgoal_tac


34 


35 
Theories


36 


37 
page 117: the three lines of ML shown can be abbreviated to just


38 
init_thy_reader();

456

39 

599

40 
page 118: extend_theory has been replaced by numerous functions for adding


41 
types, constants, axioms, etc.


42 


43 
Defining Logics

507

44 

718

45 


46 

599

47 
page 127: type constraints ("::") now have a very low priority of 4.


48 
As in ML, they must usually be enclosed in paretheses.


49 


50 
Syntax Transformations


51 


52 
page 145, line 5: delete repeated "the" in "before the the .thy file"

507

53 

716

54 
Simplification


55 

718

56 
page 157 display: Union operator is too big


57 

716

58 
page 158, "!": Isabelle now permits more general lefthand sides, so called


59 
higherorder patterns.

507

60 

872

61 
Classical reasoner


62 

1083

63 
page 176: Classical sets may specify a "wrapper tactical", which can be used


64 
to define addss. The package also provides tactics slow_tac, slow_best_tac,


65 
depth_tac and deepen_tac.

718

66 

599

67 
ISABELLE'S OBJECTLOGICS


68 

718

69 
FirstOrder Logic


70 

872

71 
pages 191, 196: FOL_dup_cs is now deleted (use deepen_tac FOL_cs instead)

718

72 

599

73 
ZermeloFraenkel Set Theory

507

74 

718

75 
page 204: type i has class term, not (just) logic


76 

599

77 
page 209: axioms have been renamed:


78 
union_iff is now Union_iff


79 
power_set is now Pow_iff

456

80 

599

81 
page 215, bottom of figure 17.10: DiffD2 is now "c : A  B ==> c ~: B"


82 


83 
page 215, bottom: rules mem_anti_sym and mem_anti_refl are now mem_asym and


84 
mem_irrefl

456

85 

599

86 
page 222, top: missing braces in qconverse_def (around righthand side)


87 
and QSigma_def (around <x;y>)


88 


89 
page 223, top: lfp_def, gfp_def have missing braces around the argument of


90 
Inter, Union

458

91 

599

92 
page 228: now there is also a theory of cardinal numbers and some


93 
developments involving the Axiom of Choice.

479

94 

599

95 
page 229: now there is another examples directory, IMP (a semantics


96 
equivalence proof for an imperative language)


97 


98 
HigherOrder Logic


99 


100 
page 243: Pow is a new constant of type 'a set => 'a set set

491

101 

599

102 
page 246: Pow is defined by Pow(A) == {B. B <= A}

863

103 
empty_def should be {} == {x.False}

599

104 


105 
page 248: Pow has the rules


106 
PowI A<=B ==> A: Pow(B)


107 
PowD A: Pow(B) ==> A<=B

507

108 

701

109 
page 251: split now has type [['a,'b] => 'c, 'a * 'b] => 'c


110 
Definition modified accordingly


111 


112 
page 252: sum_case now has type ['a=>'c,'b=>'c, 'a+'b] =>'c


113 
Definition and rules modified accordingly


114 

718

115 
page 252: HOL_dup_cs is now deleted (use deepen_tac HOL_cs instead)


116 

701

117 
page 254: nat_case now has type ['a, nat=>'a, nat] =>'a


118 
Definition modified accordingly


119 


120 
page 256,258: list_case now takes the list as its last argument, not the


121 
first.


122 

601

123 
page 259: HOL theory files may now include datatype declarations, primitive

614

124 
recursive function definitions, and (co)inductive definitions. (These new


125 
sections are available separately as the file ml/HOLextensions.dvi.gz,


126 
host ftp.cl.cam.ac.uk.)

599

127 


128 
page 259: now there is another examples directory, IMP (a semantics


129 
equivalence proof for an imperative language)
