now in a format that could be published
authorlcp
Fri Sep 09 13:10:09 1994 +0200 (1994-09-09)
changeset 59908b403fe92b1
parent 598 2457042caac8
child 600 d9133e7ed38a
now in a format that could be published
doc-src/ERRATA.txt
     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 +INTRODUCTION TO ISABELLE
    1.17 +
    1.18 +Advanced Methods
    1.19 +
    1.20 +page 52, middle: the declaration "types bool,nat" should be "types bool nat"
    1.21  
    1.22 -*page 50: In section heading, Mixfix should be mixfix
    1.23 +page 57, bottom: should be addsimps in 
    1.24 +	val add_ss = FOL_ss addrews [add_0, add_Suc]
    1.25 +
    1.26 +
    1.27 +ISABELLE REFERENCE MANUAL
    1.28  
    1.29 -*page 217 and 251: fst and snd should be fst_conv and snd_conv.
    1.30 -*Also affects index: pages 310 and 317!
    1.31 +Introduction
    1.32 +
    1.33 +page 67: show_brackets is another flag, controlling display of bracketting
    1.34 +
    1.35 +Tactics
    1.36  
    1.37 -*page 224: type of id, namely $\To i$, should be $i \To i$ 
    1.38 +page 85: subgoals_tac is another tactic, for multiple calls to subgoal_tac
    1.39 +
    1.40 +Theories
    1.41 +
    1.42 +page 117: the three lines of ML shown can be abbreviated to just
    1.43 +	init_thy_reader();
    1.44  
    1.45 -Intro/advanced
    1.46 -page 52: the declaration  "types bool,nat"  is illegal    
    1.47 +page 118: extend_theory has been replaced by numerous functions for adding
    1.48 +types, constants, axioms, etc.
    1.49 +
    1.50 +Defining Logics
    1.51  
    1.52 -should be addsimps in 'val add_ss = FOL_ss addrews [add_0, add_Suc]'
    1.53 +page 127: type constraints ("::") now have a very low priority of 4.
    1.54 +As in ML, they must usually be enclosed in paretheses.
    1.55 +
    1.56 +Syntax Transformations
    1.57 +
    1.58 +page 145, line -5: delete repeated "the" in "before the the .thy file"
    1.59  
    1.60  
    1.61 -Ref/introduction: documented show_brackets; added\pageref{sec:goals-printing}
    1.62 +ISABELLE'S OBJECT-LOGICS
    1.63 +
    1.64 +Zermelo-Fraenkel Set Theory
    1.65  
    1.66 -Ref/goals: in 'Printing the proof state' added \ref{sec:printing-control}
    1.67 +page 209: axioms have been renamed:
    1.68 +	union_iff is now Union_iff
    1.69 +	power_set is now Pow_iff
    1.70  
    1.71 -Ref/tactic: documented subgoals_tac
    1.72 +page 215, bottom of figure 17.10: DiffD2 is now  "c : A - B ==> c ~: B"
    1.73 +
    1.74 +page 215, bottom: rules mem_anti_sym and mem_anti_refl are now mem_asym and
    1.75 +mem_irrefl
    1.76  
    1.77 -Ref/theories: added init_thy_reader and removed extend_theory.
    1.78 +page 222, top: missing braces in qconverse_def (around right-hand side)
    1.79 +and QSigma_def (around <x;y>)
    1.80 +
    1.81 +page 223, top: lfp_def, gfp_def have missing braces around the argument of
    1.82 +Inter, Union
    1.83  
    1.84 -Ref/defining: type constraints ("::") now have a very low priority of 4.
    1.85 -              As in ML, they must be enclosed in paretheses most of the time.
    1.86 +page 228: now there is also a theory of cardinal numbers and some
    1.87 +developments involving the Axiom of Choice.
    1.88  
    1.89 -Ref/syntax (page 145?): deleted repeated "the" in "before the the .thy file"
    1.90 +page 229: now there is another examples directory, IMP (a semantics
    1.91 +equivalence proof for an imperative language)
    1.92 +
    1.93 +Higher-Order Logic
    1.94 +
    1.95 +page 243: Pow is a new constant of type 'a set => 'a set set
    1.96  
    1.97 -Logics/ZF: ****************
    1.98 -renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl
    1.99 -renamed union_iff to Union_iff
   1.100 -renamed power_set to Pow_iff
   1.101 -DiffD2: now is really a destruction rule
   1.102 -escaped braces in qconverse_def, QSigma_def, lfp_def, gfp_def
   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)