summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/ERRATA.txt

changeset 599 | 08b403fe92b1 |

parent 507 | a00301e9e64b |

child 601 | 208834a9ba70 |

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)