doc-src/ERRATA.txt
 author lcp Thu May 11 10:33:07 1995 +0200 (1995-05-11) changeset 1117 839ab9c054f6 parent 1083 53a0667e1cd2 child 14379 ea10a8c3e9cf permissions -rw-r--r--
show_sorts
 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@1083 ` 15` ```page 46: the theory sections can appear in any order ``` lcp@1083 ` 16` lcp@1083 ` 17` ```page 48: theories may now contain a separate definition part ``` lcp@1083 ` 18` lcp@599 ` 19` ```page 52, middle: the declaration "types bool,nat" should be "types bool nat" ``` lcp@456 ` 20` lcp@599 ` 21` ```page 57, bottom: should be addsimps in ``` lcp@599 ` 22` ``` val add_ss = FOL_ss addrews [add_0, add_Suc] ``` lcp@599 ` 23` lcp@599 ` 24` lcp@599 ` 25` ```ISABELLE REFERENCE MANUAL ``` lcp@456 ` 26` lcp@599 ` 27` ```Introduction ``` lcp@599 ` 28` lcp@599 ` 29` ```page 67: show_brackets is another flag, controlling display of bracketting ``` lcp@1117 ` 30` ```show_sorts:=true forces display of types ``` lcp@599 ` 31` lcp@599 ` 32` ```Tactics ``` lcp@456 ` 33` lcp@599 ` 34` ```page 85: subgoals_tac is another tactic, for multiple calls to subgoal_tac ``` lcp@599 ` 35` lcp@599 ` 36` ```Theories ``` lcp@599 ` 37` lcp@599 ` 38` ```page 117: the three lines of ML shown can be abbreviated to just ``` lcp@599 ` 39` ``` init_thy_reader(); ``` lcp@456 ` 40` lcp@599 ` 41` ```page 118: extend_theory has been replaced by numerous functions for adding ``` lcp@599 ` 42` ```types, constants, axioms, etc. ``` lcp@599 ` 43` lcp@599 ` 44` ```Defining Logics ``` lcp@507 ` 45` lcp@718 ` 46` lcp@718 ` 47` lcp@599 ` 48` ```page 127: type constraints ("::") now have a very low priority of 4. ``` lcp@599 ` 49` ```As in ML, they must usually be enclosed in paretheses. ``` lcp@599 ` 50` lcp@599 ` 51` ```Syntax Transformations ``` lcp@599 ` 52` lcp@599 ` 53` ```page 145, line -5: delete repeated "the" in "before the the .thy file" ``` lcp@507 ` 54` nipkow@716 ` 55` ```Simplification ``` nipkow@716 ` 56` lcp@718 ` 57` ```page 157 display: Union operator is too big ``` lcp@718 ` 58` nipkow@716 ` 59` ```page 158, "!": Isabelle now permits more general left-hand sides, so called ``` nipkow@716 ` 60` ```higher-order patterns. ``` lcp@507 ` 61` lcp@872 ` 62` ```Classical reasoner ``` lcp@872 ` 63` lcp@1083 ` 64` ```page 176: Classical sets may specify a "wrapper tactical", which can be used ``` lcp@1083 ` 65` ```to define addss. The package also provides tactics slow_tac, slow_best_tac, ``` lcp@1083 ` 66` ```depth_tac and deepen_tac. ``` lcp@718 ` 67` lcp@599 ` 68` ```ISABELLE'S OBJECT-LOGICS ``` lcp@599 ` 69` lcp@718 ` 70` ```First-Order Logic ``` lcp@718 ` 71` lcp@872 ` 72` ```pages 191, 196: FOL_dup_cs is now deleted (use deepen_tac FOL_cs instead) ``` lcp@718 ` 73` lcp@599 ` 74` ```Zermelo-Fraenkel Set Theory ``` lcp@507 ` 75` lcp@718 ` 76` ```page 204: type i has class term, not (just) logic ``` lcp@718 ` 77` lcp@599 ` 78` ```page 209: axioms have been renamed: ``` lcp@599 ` 79` ``` union_iff is now Union_iff ``` lcp@599 ` 80` ``` power_set is now Pow_iff ``` lcp@456 ` 81` lcp@599 ` 82` ```page 215, bottom of figure 17.10: DiffD2 is now "c : A - B ==> c ~: B" ``` lcp@599 ` 83` lcp@599 ` 84` ```page 215, bottom: rules mem_anti_sym and mem_anti_refl are now mem_asym and ``` lcp@599 ` 85` ```mem_irrefl ``` lcp@456 ` 86` lcp@599 ` 87` ```page 222, top: missing braces in qconverse_def (around right-hand side) ``` lcp@599 ` 88` ```and QSigma_def (around ) ``` lcp@599 ` 89` lcp@599 ` 90` ```page 223, top: lfp_def, gfp_def have missing braces around the argument of ``` lcp@599 ` 91` ```Inter, Union ``` nipkow@458 ` 92` lcp@599 ` 93` ```page 228: now there is also a theory of cardinal numbers and some ``` lcp@599 ` 94` ```developments involving the Axiom of Choice. ``` nipkow@479 ` 95` lcp@599 ` 96` ```page 229: now there is another examples directory, IMP (a semantics ``` lcp@599 ` 97` ```equivalence proof for an imperative language) ``` lcp@599 ` 98` lcp@599 ` 99` ```Higher-Order Logic ``` lcp@599 ` 100` lcp@599 ` 101` ```page 243: Pow is a new constant of type 'a set => 'a set set ``` lcp@491 ` 102` lcp@599 ` 103` ```page 246: Pow is defined by Pow(A) == {B. B <= A} ``` lcp@863 ` 104` ```empty_def should be {} == {x.False} ``` lcp@599 ` 105` lcp@599 ` 106` ```page 248: Pow has the rules ``` lcp@599 ` 107` ``` PowI A<=B ==> A: Pow(B) ``` lcp@599 ` 108` ``` PowD A: Pow(B) ==> A<=B ``` lcp@507 ` 109` lcp@701 ` 110` ```page 251: split now has type [['a,'b] => 'c, 'a * 'b] => 'c ``` lcp@701 ` 111` ```Definition modified accordingly ``` lcp@701 ` 112` lcp@701 ` 113` ```page 252: sum_case now has type ['a=>'c,'b=>'c, 'a+'b] =>'c ``` lcp@701 ` 114` ```Definition and rules modified accordingly ``` lcp@701 ` 115` lcp@718 ` 116` ```page 252: HOL_dup_cs is now deleted (use deepen_tac HOL_cs instead) ``` lcp@718 ` 117` lcp@701 ` 118` ```page 254: nat_case now has type ['a, nat=>'a, nat] =>'a ``` lcp@701 ` 119` ```Definition modified accordingly ``` lcp@701 ` 120` lcp@701 ` 121` ```page 256,258: list_case now takes the list as its last argument, not the ``` lcp@701 ` 122` ```first. ``` lcp@701 ` 123` nipkow@601 ` 124` ```page 259: HOL theory files may now include datatype declarations, primitive ``` lcp@614 ` 125` ```recursive function definitions, and (co)inductive definitions. (These new ``` lcp@614 ` 126` ```sections are available separately as the file ml/HOL-extensions.dvi.gz, ``` lcp@614 ` 127` ```host ftp.cl.cam.ac.uk.) ``` lcp@599 ` 128` lcp@599 ` 129` ```page 259: now there is another examples directory, IMP (a semantics ``` lcp@599 ` 130` ```equivalence proof for an imperative language) ```