doc-src/ERRATA.txt
author blanchet
Thu, 19 Jan 2012 21:37:12 +0100
changeset 46300 6ded25a6098a
parent 42637 381fdcab0f36
permissions -rw-r--r--
updated Sledge docs some more

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 46: the theory sections can appear in any order

page 48: theories may now contain a separate definition part

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
show_sorts:=true forces display of types

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"

Simplification

page 157 display: Union operator is too big

page 158, "!": Isabelle now permits more general left-hand sides, so called
higher-order patterns.

Classical reasoner

page 176: Classical sets may specify a "wrapper tactical", which can be used
to define addss.  The package also provides tactics slow_tac, slow_best_tac,
depth_tac and deepen_tac.

ISABELLE'S OBJECT-LOGICS

First-Order Logic

pages 191, 196: FOL_dup_cs is now deleted (use deepen_tac FOL_cs instead)

Zermelo-Fraenkel Set Theory

page 204: type i has class term, not (just) logic

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}
empty_def should be  {} == {x.False}

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 252: HOL_dup_cs is now deleted (use deepen_tac HOL_cs instead)

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 at
    http://www.cl.cam.ac.uk/users/lcp/archive/ml/HOL-extensions.dvi.gz

page 259: now there is another examples directory, IMP (a semantics
equivalence proof for an imperative language)