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)