1.1 --- a/doc-src/ERRATA.txt Fri Sep 09 12:34:54 1994 +0200
1.2 +++ b/doc-src/ERRATA.txt Fri Sep 09 13:10:09 1994 +0200
1.3 @@ -1,39 +1,88 @@
1.4 -ERRATA in Springer book
1.5 +$Id$
1.6 +ERRATA in the book "Isabelle: A Generic Theorem Prover"
1.7 +by Lawrence C. Paulson (contributions by Tobias Nipkow)
1.8 +
1.9 +Some of these errors are typographical but most of them are due to continuing
1.10 +changes to Isabelle.
1.11
1.12 Thanks to Sara Kalvala, Tobias Nipkow
1.13
1.14 -* = corrected by sending new pages
1.15
1.16 -*page 50: In section heading, Mixfix should be mixfix
1.17 +INTRODUCTION TO ISABELLE
1.18
1.19 -*page 217 and 251: fst and snd should be fst_conv and snd_conv.
1.20 -*Also affects index: pages 310 and 317!
1.21 +Advanced Methods
1.22
1.23 -*page 224: type of id, namely $\To i$, should be $i \To i$
1.24 +page 52, middle: the declaration "types bool,nat" should be "types bool nat"
1.25
1.26 -Intro/advanced
1.27 -page 52: the declaration "types bool,nat" is illegal
1.28 +page 57, bottom: should be addsimps in
1.29 + val add_ss = FOL_ss addrews [add_0, add_Suc]
1.30
1.31 -should be addsimps in 'val add_ss = FOL_ss addrews [add_0, add_Suc]'
1.32
1.33 +ISABELLE REFERENCE MANUAL
1.34
1.35 -Ref/introduction: documented show_brackets; added\pageref{sec:goals-printing}
1.36 +Introduction
1.37
1.38 -Ref/goals: in 'Printing the proof state' added \ref{sec:printing-control}
1.39 +page 67: show_brackets is another flag, controlling display of bracketting
1.40
1.41 -Ref/tactic: documented subgoals_tac
1.42 +Tactics
1.43
1.44 -Ref/theories: added init_thy_reader and removed extend_theory.
1.45 +page 85: subgoals_tac is another tactic, for multiple calls to subgoal_tac
1.46
1.47 -Ref/defining: type constraints ("::") now have a very low priority of 4.
1.48 - As in ML, they must be enclosed in paretheses most of the time.
1.49 +Theories
1.50
1.51 -Ref/syntax (page 145?): deleted repeated "the" in "before the the .thy file"
1.52 +page 117: the three lines of ML shown can be abbreviated to just
1.53 + init_thy_reader();
1.54
1.55 -Logics/ZF: ****************
1.56 -renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl
1.57 -renamed union_iff to Union_iff
1.58 -renamed power_set to Pow_iff
1.59 -DiffD2: now is really a destruction rule
1.60 -escaped braces in qconverse_def, QSigma_def, lfp_def, gfp_def
1.61 +page 118: extend_theory has been replaced by numerous functions for adding
1.62 +types, constants, axioms, etc.
1.63
1.64 +Defining Logics
1.65 +
1.66 +page 127: type constraints ("::") now have a very low priority of 4.
1.67 +As in ML, they must usually be enclosed in paretheses.
1.68 +
1.69 +Syntax Transformations
1.70 +
1.71 +page 145, line -5: delete repeated "the" in "before the the .thy file"
1.72 +
1.73 +
1.74 +ISABELLE'S OBJECT-LOGICS
1.75 +
1.76 +Zermelo-Fraenkel Set Theory
1.77 +
1.78 +page 209: axioms have been renamed:
1.79 + union_iff is now Union_iff
1.80 + power_set is now Pow_iff
1.81 +
1.82 +page 215, bottom of figure 17.10: DiffD2 is now "c : A - B ==> c ~: B"
1.83 +
1.84 +page 215, bottom: rules mem_anti_sym and mem_anti_refl are now mem_asym and
1.85 +mem_irrefl
1.86 +
1.87 +page 222, top: missing braces in qconverse_def (around right-hand side)
1.88 +and QSigma_def (around <x;y>)
1.89 +
1.90 +page 223, top: lfp_def, gfp_def have missing braces around the argument of
1.91 +Inter, Union
1.92 +
1.93 +page 228: now there is also a theory of cardinal numbers and some
1.94 +developments involving the Axiom of Choice.
1.95 +
1.96 +page 229: now there is another examples directory, IMP (a semantics
1.97 +equivalence proof for an imperative language)
1.98 +
1.99 +Higher-Order Logic
1.100 +
1.101 +page 243: Pow is a new constant of type 'a set => 'a set set
1.102 +
1.103 +page 246: Pow is defined by Pow(A) == {B. B <= A}
1.104 +
1.105 +page 248: Pow has the rules
1.106 + PowI A<=B ==> A: Pow(B)
1.107 + PowD A: Pow(B) ==> A<=B
1.108 +
1.109 +page 259: HOL theory files may now include datatype declarations and
1.110 +(co)inductive definitions. (Two sections added.)
1.111 +
1.112 +page 259: now there is another examples directory, IMP (a semantics
1.113 +equivalence proof for an imperative language)