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

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

lcp@599

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

lcp@599

43 

lcp@599

44 
Syntax Transformations

lcp@599

45 

lcp@599

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

lcp@507

47 

lcp@507

48 

lcp@599

49 
ISABELLE'S OBJECTLOGICS

lcp@599

50 

lcp@599

51 
ZermeloFraenkel Set Theory

lcp@507

52 

lcp@599

53 
page 209: axioms have been renamed:

lcp@599

54 
union_iff is now Union_iff

lcp@599

55 
power_set is now Pow_iff

lcp@456

56 

lcp@599

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

lcp@599

58 

lcp@599

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

lcp@599

60 
mem_irrefl

lcp@456

61 

lcp@599

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

lcp@599

63 
and QSigma_def (around <x;y>)

lcp@599

64 

lcp@599

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

lcp@599

66 
Inter, Union

nipkow@458

67 

lcp@599

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

lcp@599

69 
developments involving the Axiom of Choice.

nipkow@479

70 

lcp@599

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

lcp@599

72 
equivalence proof for an imperative language)

lcp@599

73 

lcp@599

74 
HigherOrder Logic

lcp@599

75 

lcp@599

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

lcp@491

77 

lcp@599

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

lcp@599

79 

lcp@599

80 
page 248: Pow has the rules

lcp@599

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

lcp@599

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

lcp@507

83 

nipkow@601

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

lcp@614

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

lcp@614

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

lcp@614

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

lcp@599

88 

lcp@599

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

lcp@599

90 
equivalence proof for an imperative language)
