$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 continuingchanges to Isabelle.Thanks to Sara Kalvala, Tobias NipkowINTRODUCTION TO ISABELLEAdvanced Methodspage 46: the theory sections can appear in any orderpage 48: theories may now contain a separate definition partpage 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 MANUALIntroductionpage 67: show_brackets is another flag, controlling display of brackettingshow_sorts:=true forces display of typesTacticspage 85: subgoals_tac is another tactic, for multiple calls to subgoal_tacTheoriespage 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 addingtypes, constants, axioms, etc.Defining Logicspage 127: type constraints ("::") now have a very low priority of 4.As in ML, they must usually be enclosed in paretheses.Syntax Transformationspage 145, line -5: delete repeated "the" in "before the the .thy file"Simplificationpage 157 display: Union operator is too bigpage 158, "!": Isabelle now permits more general left-hand sides, so calledhigher-order patterns.Classical reasonerpage 176: Classical sets may specify a "wrapper tactical", which can be usedto define addss. The package also provides tactics slow_tac, slow_best_tac,depth_tac and deepen_tac.ISABELLE'S OBJECT-LOGICSFirst-Order Logicpages 191, 196: FOL_dup_cs is now deleted (use deepen_tac FOL_cs instead)Zermelo-Fraenkel Set Theorypage 204: type i has class term, not (just) logicpage 209: axioms have been renamed: union_iff is now Union_iff power_set is now Pow_iffpage 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 andmem_irreflpage 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 ofInter, Unionpage 228: now there is also a theory of cardinal numbers and somedevelopments involving the Axiom of Choice.page 229: now there is another examples directory, IMP (a semanticsequivalence proof for an imperative language)Higher-Order Logicpage 243: Pow is a new constant of type 'a set => 'a set setpage 246: Pow is defined by Pow(A) == {B. B <= A}empty_def should be {} == {x.False}page 248: Pow has the rules PowI A<=B ==> A: Pow(B) PowD A: Pow(B) ==> A<=Bpage 251: split now has type [['a,'b] => 'c, 'a * 'b] => 'cDefinition modified accordinglypage 252: sum_case now has type ['a=>'c,'b=>'c, 'a+'b] =>'cDefinition and rules modified accordinglypage 252: HOL_dup_cs is now deleted (use deepen_tac HOL_cs instead)page 254: nat_case now has type ['a, nat=>'a, nat] =>'aDefinition modified accordinglypage 256,258: list_case now takes the list as its last argument, not thefirst.page 259: HOL theory files may now include datatype declarations, primitiverecursive function definitions, and (co)inductive definitions. These newsections are available separately at http://www.cl.cam.ac.uk/users/lcp/archive/ml/HOL-extensions.dvi.gzpage 259: now there is another examples directory, IMP (a semanticsequivalence proof for an imperative language)