summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/ERRATA.txt

author | lcp |

Fri, 11 Nov 1994 10:31:51 +0100 | |

changeset 701 | 74ee8b9ff9a7 |

parent 614 | da97045ef59a |

child 716 | 79adbdbda0fb |

permissions | -rw-r--r-- |

argument swaps in HOL

$Id$ ERRATA in the book "Isabelle: A Generic Theorem Prover" by Lawrence C. Paulson (contributions by Tobias Nipkow) Some of these errors are typographical but most of them are due to continuing changes to Isabelle. Thanks to Sara Kalvala, Tobias Nipkow INTRODUCTION TO ISABELLE Advanced Methods page 52, middle: the declaration "types bool,nat" should be "types bool nat" page 57, bottom: should be addsimps in val add_ss = FOL_ss addrews [add_0, add_Suc] ISABELLE REFERENCE MANUAL Introduction page 67: show_brackets is another flag, controlling display of bracketting Tactics page 85: subgoals_tac is another tactic, for multiple calls to subgoal_tac Theories page 117: the three lines of ML shown can be abbreviated to just init_thy_reader(); page 118: extend_theory has been replaced by numerous functions for adding types, constants, axioms, etc. Defining Logics page 127: type constraints ("::") now have a very low priority of 4. As in ML, they must usually be enclosed in paretheses. Syntax Transformations page 145, line -5: delete repeated "the" in "before the the .thy file" ISABELLE'S OBJECT-LOGICS Zermelo-Fraenkel Set Theory page 209: axioms have been renamed: union_iff is now Union_iff power_set is now Pow_iff page 215, bottom of figure 17.10: DiffD2 is now "c : A - B ==> c ~: B" page 215, bottom: rules mem_anti_sym and mem_anti_refl are now mem_asym and mem_irrefl page 222, top: missing braces in qconverse_def (around right-hand side) and QSigma_def (around <x;y>) page 223, top: lfp_def, gfp_def have missing braces around the argument of Inter, Union page 228: now there is also a theory of cardinal numbers and some developments involving the Axiom of Choice. page 229: now there is another examples directory, IMP (a semantics equivalence proof for an imperative language) Higher-Order Logic page 243: Pow is a new constant of type 'a set => 'a set set page 246: Pow is defined by Pow(A) == {B. B <= A} page 248: Pow has the rules PowI A<=B ==> A: Pow(B) PowD A: Pow(B) ==> A<=B page 251: split now has type [['a,'b] => 'c, 'a * 'b] => 'c Definition modified accordingly page 252: sum_case now has type ['a=>'c,'b=>'c, 'a+'b] =>'c Definition and rules modified accordingly page 254: nat_case now has type ['a, nat=>'a, nat] =>'a Definition modified accordingly page 256,258: list_case now takes the list as its last argument, not the first. page 259: HOL theory files may now include datatype declarations, primitive recursive function definitions, and (co)inductive definitions. (These new sections are available separately as the file ml/HOL-extensions.dvi.gz, host ftp.cl.cam.ac.uk.) page 259: now there is another examples directory, IMP (a semantics equivalence proof for an imperative language)