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@599

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

lcp@456

16 

lcp@599

17 
page 57, bottom: should be addsimps in

lcp@599

18 
val add_ss = FOL_ss addrews [add_0, add_Suc]

lcp@599

19 

lcp@599

20 

lcp@599

21 
ISABELLE REFERENCE MANUAL

lcp@456

22 

lcp@599

23 
Introduction

lcp@599

24 

lcp@599

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

lcp@599

26 

lcp@599

27 
Tactics

lcp@456

28 

lcp@599

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

lcp@599

30 

lcp@599

31 
Theories

lcp@599

32 

lcp@599

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

lcp@599

34 
init_thy_reader();

lcp@456

35 

lcp@599

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

lcp@599

37 
types, constants, axioms, etc.

lcp@599

38 

lcp@599

39 
Defining Logics

lcp@507

40 

lcp@718

41 

lcp@718

42 

lcp@599

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

lcp@599

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

lcp@599

45 

lcp@599

46 
Syntax Transformations

lcp@599

47 

lcp@599

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

lcp@507

49 

nipkow@716

50 
Simplification

nipkow@716

51 

lcp@718

52 
page 157 display: Union operator is too big

lcp@718

53 

nipkow@716

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

nipkow@716

55 
higherorder patterns.

lcp@507

56 

lcp@872

57 
Classical reasoner

lcp@872

58 

lcp@872

59 
page 176: The package also provides tactics slow_tac, slow_best_tac, depth_tac

lcp@872

60 
and deepen_tac.

lcp@718

61 

lcp@599

62 
ISABELLE'S OBJECTLOGICS

lcp@599

63 

lcp@718

64 
FirstOrder Logic

lcp@718

65 

lcp@872

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

lcp@718

67 

lcp@599

68 
ZermeloFraenkel Set Theory

lcp@507

69 

lcp@718

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

lcp@718

71 

lcp@599

72 
page 209: axioms have been renamed:

lcp@599

73 
union_iff is now Union_iff

lcp@599

74 
power_set is now Pow_iff

lcp@456

75 

lcp@599

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

lcp@599

77 

lcp@599

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

lcp@599

79 
mem_irrefl

lcp@456

80 

lcp@599

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

lcp@599

82 
and QSigma_def (around <x;y>)

lcp@599

83 

lcp@599

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

lcp@599

85 
Inter, Union

nipkow@458

86 

lcp@599

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

lcp@599

88 
developments involving the Axiom of Choice.

nipkow@479

89 

lcp@599

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

lcp@599

91 
equivalence proof for an imperative language)

lcp@599

92 

lcp@599

93 
HigherOrder Logic

lcp@599

94 

lcp@599

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

lcp@491

96 

lcp@599

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

lcp@863

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

lcp@599

99 

lcp@599

100 
page 248: Pow has the rules

lcp@599

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

lcp@599

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

lcp@507

103 

lcp@701

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

lcp@701

105 
Definition modified accordingly

lcp@701

106 

lcp@701

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

lcp@701

108 
Definition and rules modified accordingly

lcp@701

109 

lcp@718

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

lcp@718

111 

lcp@701

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

lcp@701

113 
Definition modified accordingly

lcp@701

114 

lcp@701

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

lcp@701

116 
first.

lcp@701

117 

nipkow@601

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

lcp@614

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

lcp@614

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

lcp@614

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

lcp@599

122 

lcp@599

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

lcp@599

124 
equivalence proof for an imperative language)
