lcp@599

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

lcp@599

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

lcp@599

3 

lcp@599

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

lcp@599

5 
changes to Isabelle.

lcp@456

6 

lcp@491

7 
Thanks to Sara Kalvala, Tobias Nipkow

lcp@491

8 

lcp@599

9 

lcp@599

10 
INTRODUCTION TO ISABELLE

lcp@599

11 

lcp@599

12 
Advanced Methods

lcp@599

13 

lcp@1083

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

lcp@1083

15 

lcp@1083

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

lcp@1083

17 

lcp@599

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

lcp@456

19 

lcp@599

20 
page 57, bottom: should be addsimps in

lcp@599

21 
val add_ss = FOL_ss addrews [add_0, add_Suc]

lcp@599

22 

lcp@599

23 

lcp@599

24 
ISABELLE REFERENCE MANUAL

lcp@456

25 

lcp@599

26 
Introduction

lcp@599

27 

lcp@599

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

lcp@1117

29 
show_sorts:=true forces display of types

lcp@599

30 

lcp@599

31 
Tactics

lcp@456

32 

lcp@599

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

lcp@599

34 

lcp@599

35 
Theories

lcp@599

36 

lcp@599

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

lcp@599

38 
init_thy_reader();

lcp@456

39 

lcp@599

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

lcp@599

41 
types, constants, axioms, etc.

lcp@599

42 

lcp@599

43 
Defining Logics

lcp@507

44 

lcp@718

45 

lcp@718

46 

lcp@599

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

lcp@599

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

lcp@599

49 

lcp@599

50 
Syntax Transformations

lcp@599

51 

lcp@599

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

lcp@507

53 

nipkow@716

54 
Simplification

nipkow@716

55 

lcp@718

56 
page 157 display: Union operator is too big

lcp@718

57 

nipkow@716

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

nipkow@716

59 
higherorder patterns.

lcp@507

60 

lcp@872

61 
Classical reasoner

lcp@872

62 

lcp@1083

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

lcp@1083

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

lcp@1083

65 
depth_tac and deepen_tac.

lcp@718

66 

lcp@599

67 
ISABELLE'S OBJECTLOGICS

lcp@599

68 

lcp@718

69 
FirstOrder Logic

lcp@718

70 

lcp@872

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

lcp@718

72 

lcp@599

73 
ZermeloFraenkel Set Theory

lcp@507

74 

lcp@718

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

lcp@718

76 

lcp@599

77 
page 209: axioms have been renamed:

lcp@599

78 
union_iff is now Union_iff

lcp@599

79 
power_set is now Pow_iff

lcp@456

80 

lcp@599

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

lcp@599

82 

lcp@599

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

lcp@599

84 
mem_irrefl

lcp@456

85 

lcp@599

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

lcp@599

87 
and QSigma_def (around <x;y>)

lcp@599

88 

lcp@599

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

lcp@599

90 
Inter, Union

nipkow@458

91 

lcp@599

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

lcp@599

93 
developments involving the Axiom of Choice.

nipkow@479

94 

lcp@599

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

lcp@599

96 
equivalence proof for an imperative language)

lcp@599

97 

lcp@599

98 
HigherOrder Logic

lcp@599

99 

lcp@599

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

lcp@491

101 

lcp@599

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

lcp@863

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

lcp@599

104 

lcp@599

105 
page 248: Pow has the rules

lcp@599

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

lcp@599

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

lcp@507

108 

lcp@701

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

lcp@701

110 
Definition modified accordingly

lcp@701

111 

lcp@701

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

lcp@701

113 
Definition and rules modified accordingly

lcp@701

114 

lcp@718

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

lcp@718

116 

lcp@701

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

lcp@701

118 
Definition modified accordingly

lcp@701

119 

lcp@701

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

lcp@701

121 
first.

lcp@701

122 

nipkow@601

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

paulson@14379

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

paulson@14379

125 
sections are available separately at

paulson@14379

126 
http://www.cl.cam.ac.uk/users/lcp/archive/ml/HOLextensions.dvi.gz

lcp@599

127 

lcp@599

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

lcp@599

129 
equivalence proof for an imperative language)
