lcp@599

1 
$Id$

lcp@599

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

lcp@599

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

lcp@599

4 

lcp@599

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

lcp@599

6 
changes to Isabelle.

lcp@456

7 

lcp@491

8 
Thanks to Sara Kalvala, Tobias Nipkow

lcp@491

9 

lcp@599

10 

lcp@599

11 
INTRODUCTION TO ISABELLE

lcp@599

12 

lcp@599

13 
Advanced Methods

lcp@599

14 

lcp@1083

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

lcp@1083

16 

lcp@1083

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

lcp@1083

18 

lcp@599

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

lcp@456

20 

lcp@599

21 
page 57, bottom: should be addsimps in

lcp@599

22 
val add_ss = FOL_ss addrews [add_0, add_Suc]

lcp@599

23 

lcp@599

24 

lcp@599

25 
ISABELLE REFERENCE MANUAL

lcp@456

26 

lcp@599

27 
Introduction

lcp@599

28 

lcp@599

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

lcp@1117

30 
show_sorts:=true forces display of types

lcp@599

31 

lcp@599

32 
Tactics

lcp@456

33 

lcp@599

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

lcp@599

35 

lcp@599

36 
Theories

lcp@599

37 

lcp@599

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

lcp@599

39 
init_thy_reader();

lcp@456

40 

lcp@599

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

lcp@599

42 
types, constants, axioms, etc.

lcp@599

43 

lcp@599

44 
Defining Logics

lcp@507

45 

lcp@718

46 

lcp@718

47 

lcp@599

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

lcp@599

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

lcp@599

50 

lcp@599

51 
Syntax Transformations

lcp@599

52 

lcp@599

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

lcp@507

54 

nipkow@716

55 
Simplification

nipkow@716

56 

lcp@718

57 
page 157 display: Union operator is too big

lcp@718

58 

nipkow@716

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

nipkow@716

60 
higherorder patterns.

lcp@507

61 

lcp@872

62 
Classical reasoner

lcp@872

63 

lcp@1083

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

lcp@1083

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

lcp@1083

66 
depth_tac and deepen_tac.

lcp@718

67 

lcp@599

68 
ISABELLE'S OBJECTLOGICS

lcp@599

69 

lcp@718

70 
FirstOrder Logic

lcp@718

71 

lcp@872

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

lcp@718

73 

lcp@599

74 
ZermeloFraenkel Set Theory

lcp@507

75 

lcp@718

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

lcp@718

77 

lcp@599

78 
page 209: axioms have been renamed:

lcp@599

79 
union_iff is now Union_iff

lcp@599

80 
power_set is now Pow_iff

lcp@456

81 

lcp@599

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

lcp@599

83 

lcp@599

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

lcp@599

85 
mem_irrefl

lcp@456

86 

lcp@599

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

lcp@599

88 
and QSigma_def (around <x;y>)

lcp@599

89 

lcp@599

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

lcp@599

91 
Inter, Union

nipkow@458

92 

lcp@599

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

lcp@599

94 
developments involving the Axiom of Choice.

nipkow@479

95 

lcp@599

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

lcp@599

97 
equivalence proof for an imperative language)

lcp@599

98 

lcp@599

99 
HigherOrder Logic

lcp@599

100 

lcp@599

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

lcp@491

102 

lcp@599

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

lcp@863

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

lcp@599

105 

lcp@599

106 
page 248: Pow has the rules

lcp@599

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

lcp@599

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

lcp@507

109 

lcp@701

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

lcp@701

111 
Definition modified accordingly

lcp@701

112 

lcp@701

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

lcp@701

114 
Definition and rules modified accordingly

lcp@701

115 

lcp@718

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

lcp@718

117 

lcp@701

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

lcp@701

119 
Definition modified accordingly

lcp@701

120 

lcp@701

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

lcp@701

122 
first.

lcp@701

123 

nipkow@601

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

paulson@14379

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

paulson@14379

126 
sections are available separately at

paulson@14379

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

lcp@599

128 

lcp@599

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

lcp@599

130 
equivalence proof for an imperative language)
