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

1117

30 
show_sorts:=true forces display of types

599

31 


32 
Tactics

456

33 

599

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


35 


36 
Theories


37 


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


39 
init_thy_reader();

456

40 

599

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


42 
types, constants, axioms, etc.


43 


44 
Defining Logics

507

45 

718

46 


47 

599

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


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


50 


51 
Syntax Transformations


52 


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

507

54 

716

55 
Simplification


56 

718

57 
page 157 display: Union operator is too big


58 

716

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


60 
higherorder patterns.

507

61 

872

62 
Classical reasoner


63 

1083

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


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


66 
depth_tac and deepen_tac.

718

67 

599

68 
ISABELLE'S OBJECTLOGICS


69 

718

70 
FirstOrder Logic


71 

872

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

718

73 

599

74 
ZermeloFraenkel Set Theory

507

75 

718

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


77 

599

78 
page 209: axioms have been renamed:


79 
union_iff is now Union_iff


80 
power_set is now Pow_iff

456

81 

599

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


83 


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


85 
mem_irrefl

456

86 

599

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


88 
and QSigma_def (around <x;y>)


89 


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


91 
Inter, Union

458

92 

599

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


94 
developments involving the Axiom of Choice.

479

95 

599

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


97 
equivalence proof for an imperative language)


98 


99 
HigherOrder Logic


100 


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

491

102 

599

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

863

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

599

105 


106 
page 248: Pow has the rules


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


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

507

109 

701

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


111 
Definition modified accordingly


112 


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


114 
Definition and rules modified accordingly


115 

718

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


117 

701

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


119 
Definition modified accordingly


120 


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


122 
first.


123 

601

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

614

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


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


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

599

128 


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


130 
equivalence proof for an imperative language)
