New in this Isabelle version

 New in Isabelle2009 (April 2009)

 ----------------------------

 --------------------------------

 old ~/isabelle, which was slightly non-standard and apt cause

 old ~/isabelle, which was slightly non-standard and apt to cause

 surprises on case-insensitive file-systems.

 surprises on case-insensitive file-systems (such as Mac OS).

 Isabelle distribution.

 Isabelle distribution, in order to use the new ~/.isabelle uniformly.

 multi-core systems.  A speedup factor of 2-3 can be expected on a

 multi-core systems.  A speedup factor of 2.5 to 3.2 can be expected on

 regular 4-core machine, if the initial heap space is made reasonably

 a regular 4-core machine, if the initial heap space is made reasonably

 large (cf. Poly/ML option -H).  [Poly/ML 5.2.1 or later]

 large (cf. Poly/ML option -H).  (Requires Poly/ML 5.2.1 or later.)

 * Generalized Isar history, with support for linear undo, direct state

 * The main reference manuals ("isar-ref", "implementation", and

 addressing etc.

 "system") have been updated and extended.  Formally checked references

 as hyperlinks are now available uniformly.

 * Recovered hiding of consts, which was accidentally broken in

 Isabelle2007.  Potential INCOMPATIBILITY, ``hide const c'' really

 makes c inaccessible; consider using ``hide (open) const c'' instead.

 * Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML

 interface instead.

 * There is a new syntactic category "float_const" for signed decimal

 fractions (e.g. 123.45 or -123.45).

 * New prover for coherent logic (see src/Tools/coherent.ML).

 * Class declaration: sc. "base sort" must not be given in import list

 * Complete re-implementation of locales.  INCOMPATIBILITY in several

 any longer but is inferred from the specification.  Particularly in HOL,

 respects.  The most important changes are listed below.  See the

 write

 Tutorial on Locales ("locales" manual) for details.

     class foo = ...     instead of      class foo = type + ...

 - In locale expressions, instantiation replaces renaming.  Parameters

 must be declared in a for clause.  To aid compatibility with previous

 * Module moves in repository:

 parameter inheritance, in locale declarations, parameters that are not

     src/Pure/Tools/value.ML ~> src/Tools/

 'touched' (instantiation position "_" or omitted) are implicitly added

     src/Pure/Tools/quickcheck.ML ~> src/Tools/

 with their syntax at the beginning of the for clause.

 * Slightly more coherent Pure syntax, with updated documentation in

 - Syntax from abbreviations and definitions in locales is available in

 isar-ref manual.  Removed locales meta_term_syntax and

 locale expressions and context elements.  The latter is particularly

 meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,

 useful in locale declarations.

 INCOMPATIBILITY in rare situations.

 - More flexible mechanisms to qualify names generated by locale

 * Goal-directed proof now enforces strict proof irrelevance wrt. sort

 expressions.  Qualifiers (prefixes) may be specified in locale

 hypotheses.  Sorts required in the course of reasoning need to be

 expressions, and can be marked as mandatory (syntax: "name!:") or

 covered by the constraints in the initial statement, completed by the

 optional (syntax "name?:").  The default depends for plain "name:"

 type instance information of the background theory.  Non-trivial sort

 depends on the situation where a locale expression is used: in

 hypotheses, which rarely occur in practice, may be specified via

 commands 'locale' and 'sublocale' prefixes are optional, in

 vacuous propositions of the form SORT_CONSTRAINT('a::c).  For example:

 'interpretation' and 'interpret' prefixes are mandatory.  The old

 implicit qualifiers derived from the parameter names of a locale are

   lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ...

 no longer generated.

 The result contains an implicit sort hypotheses as before --

 - Command "sublocale l < e" replaces "interpretation l < e".  The

 SORT_CONSTRAINT premises are eliminated as part of the canonical rule

 instantiation clause in "interpretation" and "interpret" (square

 normalization.

 brackets) is no longer available.  Use locale expressions.

 * Changed defaults for unify configuration options:

 - When converting proof scripts, mandatory qualifiers in

 'interpretation' and 'interpret' should be retained by default, even

   unify_trace_bound = 50 (formerly 25)

 if this is an INCOMPATIBILITY compared to former behavior.  In the

   unify_search_bound = 60 (formerly 30)

 worst case, use the "name?:" form for non-mandatory ones.  Qualifiers

 in locale expressions range over a single locale instance only.

 * Different bookkeeping for code equations (INCOMPATIBILITY):

 - Dropped locale element "includes".  This is a major INCOMPATIBILITY.

   a) On theory merge, the last set of code equations for a particular

      constant is taken (in accordance with the policy applied by other

      parts of the code generator framework).

   b) Code equations stemming from explicit declarations (e.g. code

      attribute) gain priority over default code equations stemming

      from definition, primrec, fun etc.

 * Global versions of theorems stemming from classes do not carry a

 parameter prefix any longer.  INCOMPATIBILITY.

 * Dropped locale element "includes".  This is a major INCOMPATIBILITY.

 * Dropped "locale (open)".  INCOMPATIBILITY.

 - Discontinued "locale (open)".  INCOMPATIBILITY.

 * Interpretation commands no longer attempt to simplify goal.

 - Locale interpretation commands no longer attempt to simplify goal.

 * Interpretation commands no longer accept interpretation attributes.

 - Locale interpretation commands no longer accept interpretation

 INCOMPATBILITY.

 attributes.  INCOMPATIBILITY.

 * Complete re-implementation of locales.  INCOMPATIBILITY.  The most

 * Class declaration: so-called "base sort" must not be given in import

 important changes are listed below.  See the Tutorial on Locales for

 list any longer, but is inferred from the specification.  Particularly

 details.

 in HOL, write

 - In locale expressions, instantiation replaces renaming.  Parameters

     class foo = ...

 must be declared in a for clause.  To aid compatibility with previous

 parameter inheritance, in locale declarations, parameters that are not

 instead of

 'touched' (instantiation position "_" or omitted) are implicitly added

 with their syntax at the beginning of the for clause.

     class foo = type + ...

 - Syntax from abbreviations and definitions in locales is available in

 * Class target: global versions of theorems stemming do not carry a

 locale expressions and context elements.  The latter is particularly

 parameter prefix any longer.  INCOMPATIBILITY.

 useful in locale declarations.

 * Class 'instance' command no longer accepts attached definitions.

 - More flexible mechanisms to qualify names generated by locale

 INCOMPATIBILITY, use proper 'instantiation' target instead.

 expressions.  Qualifiers (prefixes) may be specified in locale

 expressions, and can be marked as mandatory (syntax: "name!:") or

 * Recovered hiding of consts, which was accidentally broken in

 optional (syntax "name?:").  The default depends for plain "name:"

 Isabelle2007.  Potential INCOMPATIBILITY, ``hide const c'' really

 depends on the situation where a locale expression is used: in

 makes c inaccessible; consider using ``hide (open) const c'' instead.

 commands 'locale' and 'sublocale' prefixes are optional, in

 'interpretation' and 'interpret' prefixes are mandatory.  Old-style

 * Slightly more coherent Pure syntax, with updated documentation in

 implicit qualifiers derived from the parameter names of a locale are

 isar-ref manual.  Removed locales meta_term_syntax and

 no longer generated.

 meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,

 INCOMPATIBILITY in rare situations.  Note that &&& should not be used

 - "sublocale l < e" replaces "interpretation l < e".  The

 directly in regular applications.

 instantiation clause in "interpretation" and "interpret" (square

 brackets) is no longer available.  Use locale expressions.

 * There is a new syntactic category "float_const" for signed decimal

 fractions (e.g. 123.45 or -123.45).

 - When converting proof scripts, be sure to mandatory qualifiers in

 'interpretation' and 'interpret' should be retained by default, even

 * Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML

 if this is an INCOMPATIBILITY compared to former behaviour.

 interface with 'setup' command instead.

 Qualifiers in locale expressions range over a single locale instance

 only.

 * Command 'local_setup' is similar to 'setup', but operates on a local

 theory context.

 * Command 'instance': attached definitions no longer accepted.

 INCOMPATIBILITY, use proper 'instantiation' target.

 * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.

 * New 'find_theorems' criterion "solves" matching theorems that

 * Goal-directed proof now enforces strict proof irrelevance wrt. sort

 directly solve the current goal.

 hypotheses.  Sorts required in the course of reasoning need to be

 covered by the constraints in the initial statement, completed by the

 * Auto solve feature for main theorem statements (cf. option in Proof

 type instance information of the background theory.  Non-trivial sort

 General Isabelle settings menu, disabled by default).  Whenever a new

 hypotheses, which rarely occur in practice, may be specified via

 goal is stated, "find_theorems solves" is called; any theorems that

 vacuous propositions of the form SORT_CONSTRAINT('a::c).  For example:

 could solve the lemma directly are listed as part of the goal state.

   lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ...

 The result contains an implicit sort hypotheses as before --

 SORT_CONSTRAINT premises are eliminated as part of the canonical rule

 normalization.

 * Generalized Isar history, with support for linear undo, direct state

 addressing etc.

 * Changed defaults for unify configuration options:

   unify_trace_bound = 50 (formerly 25)

   unify_search_bound = 60 (formerly 30)

 * Different bookkeeping for code equations (INCOMPATIBILITY):

   a) On theory merge, the last set of code equations for a particular

      constant is taken (in accordance with the policy applied by other

      parts of the code generator framework).

   b) Code equations stemming from explicit declarations (e.g. code

      attribute) gain priority over default code equations stemming

      from definition, primrec, fun etc.

 * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.

 * Unified theorem tables for both code code generators.  Thus [code

 func] has disappeared and only [code] remains.  INCOMPATIBILITY.

 * Command 'local_setup' is similar to 'setup', but operates on a local

 * New 'find_theorems' criterion "solves" matches theorems that

 theory context.

 directly solve the current goal (modulo higher-order unification).

 * Auto solve feature for main theorem statements: whenever a new goal

 is stated, "find_theorems solves" is called; any theorems that could

 solve the lemma directly are listed as part of the goal state.

 Cf. associated options in Proof General Isabelle settings menu,

 enabled by default, with reasonable timeout for pathological cases of

 higher-order unification.

 * Theory Library/Polynomial.thy defines an abstract type 'a poly of

 * Integrated main parts of former image HOL-Complex with HOL.  Entry

 univariate polynomials with coefficients of type 'a.  In addition to

 points Main and Complex_Main remain as before.

 the standard ring operations, it also supports div and mod.  Code

 generation is also supported, using list-style constructors.

 * Logic image HOL-Plain provides a minimal HOL with the most important

 tools available (inductive, datatype, primrec, ...).  This facilitates

 * Theory Library/Inner_Product.thy defines a class of real_inner for

 experimentation and tool development.  Note that user applications

 real inner product spaces, with an overloaded operation inner :: 'a =>

 (and library theories) should never refer to anything below theory

 'a => real.  Class real_inner is a subclass of real_normed_vector from

 Main, as before.

 RealVector.thy.

 * Logic image HOL-Main stops at theory Main, and thus facilitates

 * Theory Library/Product_Vector.thy provides instances for the product

 experimentation due to shorter build times.

 type 'a * 'b of several classes from RealVector.thy and

 Inner_Product.thy.  Definitions of addition, subtraction, scalar

 * Logic image HOL-NSA contains theories of nonstandard analysis which

 multiplication, norms, and inner products are included.

 were previously part of former HOL-Complex.  Entry point Hyperreal

 remains valid, but theories formerly using Complex_Main should now use

 * Theory Library/Bit.thy defines the field "bit" of integers modulo 2.

 new entry point Hypercomplex.

 In addition to the field operations, numerals and case syntax are also

 supported.

 * Generic ATP manager for Sledgehammer, based on ML threads instead of

 Posix processes.  Avoids potentially expensive forking of the ML

 * Theory Library/Diagonalize.thy provides constructive version of

 process.  New thread-based implementation also works on non-Unix

 Cantor's first diagonalization argument.

 platforms (Cygwin).  Provers are no longer hardwired, but defined

 within the theory via plain ML wrapper functions.  Basic Sledgehammer

 * New predicate "strict_mono" classifies strict functions on partial orders.

 commands are covered in the isar-ref manual.

 With strict functions on linear orders, reasoning about (in)equalities is

 facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less".

 * Wrapper scripts for remote SystemOnTPTP service allows to use

 sledgehammer without local ATP installation (Vampire etc.). Other

 * Some set operations are now proper qualified constants with authentic syntax.

 provers may be included via suitable ML wrappers, see also

 INCOMPATIBILITY:

 src/HOL/ATP_Linkup.thy.

 * ATP selection (E/Vampire/Spass) is now via Proof General's settings

 menu.

 * The metis method no longer fails because the theorem is too trivial

 (contains the empty clause).

 * The metis method now fails in the usual manner, rather than raising

 an exception, if it determines that it cannot prove the theorem.

 * Method "coherent" implements a prover for coherent logic (see also

 src/Tools/coherent.ML).

 * Constants "undefined" and "default" replace "arbitrary".  Usually

 "undefined" is the right choice to replace "arbitrary", though

 logically there is no difference.  INCOMPATIBILITY.

 * Command "value" now integrates different evaluation mechanisms.  The

 result of the first successful evaluation mechanism is printed.  In

 square brackets a particular named evaluation mechanisms may be

 specified (currently, [SML], [code] or [nbe]).  See further

 src/HOL/ex/Eval_Examples.thy.

 * Normalization by evaluation now allows non-leftlinear equations.

 Declare with attribute [code nbe].

 * Methods "case_tac" and "induct_tac" now refer to the very same rules

 as the structured Isar versions "cases" and "induct", cf. the

 corresponding "cases" and "induct" attributes.  Mutual induction rules

 are now presented as a list of individual projections

 (e.g. foo_bar.inducts for types foo and bar); the old format with

 explicit HOL conjunction is no longer supported.  INCOMPATIBILITY, in

 rare situations a different rule is selected --- notably nested tuple

 elimination instead of former prod.exhaust: use explicit (case_tac t

 rule: prod.exhaust) here.

 * Attributes "cases", "induct", "coinduct" support "del" option.

 * Removed fact "case_split_thm", which duplicates "case_split".

 * The option datatype has been moved to a new theory Option.  Renamed

 option_map to Option.map, and o2s to Option.set, INCOMPATIBILITY.

 * New predicate "strict_mono" classifies strict functions on partial

 orders.  With strict functions on linear orders, reasoning about

 (in)equalities is facilitated by theorems "strict_mono_eq",

 "strict_mono_less_eq" and "strict_mono_less".

 * Some set operations are now proper qualified constants with

 authentic syntax.  INCOMPATIBILITY:

 * Class complete_lattice with operations Inf, Sup, INFI, SUPR now in theory

 * Class complete_lattice with operations Inf, Sup, INFI, SUPR now in

 Set.

 theory Set.

 * Auxiliary class "itself" has disappeared -- classes without any parameter

 * Auxiliary class "itself" has disappeared -- classes without any

 are treated as expected by the 'class' command.

 parameter are treated as expected by the 'class' command.

 * Common decision procedures (Cooper, MIR, Ferrack, Approximation, Dense_Linear_Order)

 * Common decision procedures (Cooper, MIR, Ferrack, Approximation,

 now in directory HOL/Decision_Procs.

 Dense_Linear_Order) are now in directory HOL/Decision_Procs.

 * Theory HOL/Decision_Procs/Approximation.thy provides the new proof method

 * Theory src/HOL/Decision_Procs/Approximation provides the new proof

 "approximation".  It proves formulas on real values by using interval arithmetic.

 method "approximation".  It proves formulas on real values by using

 In the formulas are also the transcendental functions sin, cos, tan, atan, ln,

 interval arithmetic.  In the formulas are also the transcendental

 exp and the constant pi are allowed. For examples see

 functions sin, cos, tan, atan, ln, exp and the constant pi are

 HOL/Descision_Procs/ex/Approximation_Ex.thy.

 allowed. For examples see

 src/HOL/Descision_Procs/ex/Approximation_Ex.thy.

 * Entry point to Word library now simply named "Word".  INCOMPATIBILITY.

 * Entry point to Word library now simply named "Word".

 INCOMPATIBILITY.

 * If methods "eval" and "evaluation" encounter a structured proof state

 * If methods "eval" and "evaluation" encounter a structured proof

 with !!/==>, only the conclusion is evaluated to True (if possible),

 state with !!/==>, only the conclusion is evaluated to True (if

 avoiding strange error messages.

 possible), avoiding strange error messages.

 * Simplifier: simproc for let expressions now unfolds if bound variable

 * Method "sizechange" automates termination proofs using (a

 occurs at most once in let expression body.  INCOMPATIBILITY.

 modification of) the size-change principle.  Requires SAT solver.  See

 src/HOL/ex/Termination.thy for examples.

 * New attribute "arith" for facts that should always be used automaticaly

 by arithmetic. It is intended to be used locally in proofs, eg

 * Simplifier: simproc for let expressions now unfolds if bound

 assumes [arith]: "x > 0"

 variable occurs at most once in let expression body.  INCOMPATIBILITY.

 * Method "arith": Linear arithmetic now ignores all inequalities when

 fast_arith_neq_limit is exceeded, instead of giving up entirely.

 * New attribute "arith" for facts that should always be used

 automatically by arithmetic. It is intended to be used locally in

 proofs, e.g.

   assumes [arith]: "x > 0"

 * New classes "top" and "bot" with corresponding operations "top" and "bot"

 * New classes "top" and "bot" with corresponding operations "top" and

 in theory Orderings;  instantiation of class "complete_lattice" requires

 "bot" in theory Orderings; instantiation of class "complete_lattice"

 instantiation of classes "top" and "bot".  INCOMPATIBILITY.

 requires instantiation of classes "top" and "bot".  INCOMPATIBILITY.

 * Changed definition lemma "less_fun_def" in order to provide an instance

 * Changed definition lemma "less_fun_def" in order to provide an

 for preorders on functions;  use lemma "less_le" instead.  INCOMPATIBILITY.

 instance for preorders on functions; use lemma "less_le" instead.

 INCOMPATIBILITY.

 * Unified theorem tables for both code code generators.  Thus

 [code func] has disappeared and only [code] remains.  INCOMPATIBILITY.

 * Theory Orderings: class "wellorder" moved here, with explicit

 induction rule "less_induct" as assumption.  For instantiation of

 * Constants "undefined" and "default" replace "arbitrary".  Usually

 "wellorder" by means of predicate "wf", use rule wf_wellorderI.

 "undefined" is the right choice to replace "arbitrary", though logically

 INCOMPATIBILITY.

 there is no difference.  INCOMPATIBILITY.

 * Theory Orderings: added class "preorder" as superclass of "order".

 * Generic ATP manager for Sledgehammer, based on ML threads instead of

 Posix processes.  Avoids potentially expensive forking of the ML

 process.  New thread-based implementation also works on non-Unix

 platforms (Cygwin).  Provers are no longer hardwired, but defined

 within the theory via plain ML wrapper functions.  Basic Sledgehammer

 commands are covered in the isar-ref manual.

 * Wrapper scripts for remote SystemOnTPTP service allows to use

 sledgehammer without local ATP installation (Vampire etc.). Other

 provers may be included via suitable ML wrappers, see also

 src/HOL/ATP_Linkup.thy.

 * Normalization by evaluation now allows non-leftlinear equations.

 Declare with attribute [code nbe].

 * Command "value" now integrates different evaluation

 mechanisms.  The result of the first successful evaluation mechanism

 is printed.  In square brackets a particular named evaluation

 mechanisms may be specified (currently, [SML], [code] or [nbe]).  See

 further src/HOL/ex/Eval_Examples.thy.

 * New method "sizechange" to automate termination proofs using (a

 modification of) the size-change principle. Requires SAT solver. See

 src/HOL/ex/Termination.thy for examples.

 * HOL/Orderings: class "wellorder" moved here, with explicit induction

 rule "less_induct" as assumption.  For instantiation of "wellorder" by

 means of predicate "wf", use rule wf_wellorderI.  INCOMPATIBILITY.

 * HOL/Orderings: added class "preorder" as superclass of "order".

 * HOL/Relation:

 * Theory Relation: renamed "refl" to "refl_on", "reflexive" to "refl,

 Renamed "refl" to "refl_on", "reflexive" to "refl, "diag" to "Id_on".

 "diag" to "Id_on".

 * HOL/Finite_Set: added a new fold combinator of type

 * Theory Finite_Set: added a new fold combinator of type

 Occasionally this is more convenient than the old fold combinator which is

 now defined in terms of the new one and renamed to fold_image.

 Occasionally this is more convenient than the old fold combinator

 which is now defined in terms of the new one and renamed to

 * HOL/Ring_and_Field and HOL/OrderedGroup: The lemmas "group_simps" and

 fold_image.

 "ring_simps" have been replaced by "algebra_simps" (which can be extended with

 further lemmas!). At the moment both still exist but the former will disappear

 * Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps"

 at some point.

 and "ring_simps" have been replaced by "algebra_simps" (which can be

 extended with further lemmas!).  At the moment both still exist but

 * HOL/Power: Lemma power_Suc is now declared as a simp rule in class

 the former will disappear at some point.

 recpower.  Type-specific simp rules for various recpower types have

 been removed.  INCOMPATIBILITY.  Rename old lemmas as follows:

 * Theory Power: Lemma power_Suc is now declared as a simp rule in

 class recpower.  Type-specific simp rules for various recpower types

 have been removed.  INCOMPATIBILITY, rename old lemmas as follows:

 * HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been

 * Theories Ring_and_Field and Divides: Definition of "op dvd" has been

 * HOL/IntDiv: removed many lemmas that are instances of class-based

 * Theory IntDiv: removed many lemmas that are instances of class-based

 generalizations (from Divides and Ring_and_Field).

 generalizations (from Divides and Ring_and_Field).  INCOMPATIBILITY,

 INCOMPATIBILITY. Rename old lemmas as follows:

 rename old lemmas as follows:

 * HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,

 * Theory Rational: 'Fract k 0' now equals '0'.  INCOMPATIBILITY.

 * The real numbers offer decimal input syntax: 12.34 is translated

 into 1234/10^2. This translation is not reversed upon output.

 * Theory Library/Polynomial defines an abstract type 'a poly of

 univariate polynomials with coefficients of type 'a.  In addition to

 the standard ring operations, it also supports div and mod.  Code

 generation is also supported, using list-style constructors.

 * Theory Library/Inner_Product defines a class of real_inner for real

 inner product spaces, with an overloaded operation inner :: 'a => 'a

 => real.  Class real_inner is a subclass of real_normed_vector from

 theory RealVector.

 * Theory Library/Product_Vector provides instances for the product

 type 'a * 'b of several classes from RealVector and Inner_Product.

 Definitions of addition, subtraction, scalar multiplication, norms,

 and inner products are included.

 * Theory Library/Bit defines the field "bit" of integers modulo 2.  In

 addition to the field operations, numerals and case syntax are also

 supported.

 * Theory Library/Diagonalize provides constructive version of Cantor's

 first diagonalization argument.

 * Theory Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,

 the HOL Distribution.  zgcd and zlcm replace former igcd and ilcm;

 the HOL Distribution.  Constants zgcd and zlcm replace former igcd and

 corresponding theorems renamed accordingly.  INCOMPATIBILITY.  To

 ilcm; corresponding theorems renamed accordingly.  INCOMPATIBILITY,

 recover tupled syntax, use syntax declarations like:

 may recover tupled syntax as follows:

 (analogously for lcm, zgcd, zlcm).

 The same works for lcm, zgcd, zlcm.

 * HOL/Real/Rational: 'Fract k 0' now equals '0'.  INCOMPATIBILITY.

 * Theory Library/Nat_Infinity: added addition, numeral syntax and more

 instantiations for algebraic structures.  Removed some duplicate

 * The real numbers offer decimal input syntax: 12.34 is translated into

 theorems.  Changes in simp rules.  INCOMPATIBILITY.

   1234/10^2. This translation is not reversed upon output.

 * ML antiquotation @{code} takes a constant as argument and generates

 * New ML antiquotation @{code}: takes constant as argument, generates

 instrumentalizing code generation.  See HOL/Decision_Procs/Ferrack for

 instrumentalizing code generation.  See

 a more ambitious application.  In future you ought refrain from ad-hoc

 src/HOL/Decision_Procs/Ferrack.thy for a more ambitious application.

 compiling generated SML code on the ML toplevel.  Note that (for technical

 In future you ought to refrain from ad-hoc compiling generated SML

 reasons) @{code} cannot refer to constants for which user-defined

 code on the ML toplevel.  Note that (for technical reasons) @{code}

 serializations are set.  Refer to the corresponding ML counterpart

 cannot refer to constants for which user-defined serializations are

 directly in that cases.

 set.  Refer to the corresponding ML counterpart directly in that

 cases.

 * Integrated image HOL-Complex with HOL.  Entry points Main.thy and

 Complex_Main.thy remain as they are.

 * New image HOL-Plain provides a minimal HOL with the most important

 tools available (inductive, datatype, primrec, ...).  By convention

 the corresponding theory Plain should be ancestor of every further

 (library) theory.  Some library theories now have ancestor Plain

 (instead of Main), thus theory Main occasionally has to be imported

 explicitly.

 * The metis method now fails in the usual manner, rather than raising

 an exception, if it determines that it cannot prove the theorem.

 * The metis method no longer fails because the theorem is too trivial

 (contains the empty clause).

 * Methods "case_tac" and "induct_tac" now refer to the very same rules

 as the structured Isar versions "cases" and "induct", cf. the

 corresponding "cases" and "induct" attributes.  Mutual induction rules

 are now presented as a list of individual projections

 (e.g. foo_bar.inducts for types foo and bar); the old format with

 explicit HOL conjunction is no longer supported.  INCOMPATIBILITY, in

 rare situations a different rule is selected --- notably nested tuple

 elimination instead of former prod.exhaust: use explicit (case_tac t

 rule: prod.exhaust) here.

 * Attributes "cases", "induct", "coinduct" support "del" option.

 * Removed fact "case_split_thm", which duplicates "case_split".

 * Units_l_inv and Units_r_inv are now simprules by default.

 * Units_l_inv and Units_r_inv are now simp rules by default.

 * Renamed the following theorems.  INCOMPATIBILITY.

 * Renamed the following theorems, INCOMPATIBILITY:

 * The syntax of the fixrec package has changed.  The specification

 * The syntax of the fixrec package now conforms to the general

 syntax now conforms in style to definition, primrec, function, etc.

 specification format of inductive, primrec, function, etc.  See

 See HOLCF/ex/Fixrec_ex.thy for examples.  INCOMPATIBILITY.

 src/HOLCF/ex/Fixrec_ex.thy for examples.  INCOMPATIBILITY.

 *** ZF ***

 * Proof of Zorn's Lemma for partial orders.

 delicate details of mutexes and condition variables.  [Poly/ML 5.2.1

 delicate details of mutexes and condition variables.  (Requires

 or later]

 Poly/ML 5.2.1 or later.)

 * ML bindings produced via Isar commands are stored within the Isar

 context (theory or proof).  Consequently, commands like 'use' and 'ML'

 become thread-safe and work with undo as expected (concerning

 top-level bindings, not side-effects on global references).

 INCOMPATIBILITY, need to provide proper Isar context when invoking the

 compiler at runtime; really global bindings need to be given outside a

 theory.  (Requires Poly/ML 5.2 or later.)

 * Command 'ML_prf' is analogous to 'ML' but works within a proof

 context.  Top-level ML bindings are stored within the proof context in

 a purely sequential fashion, disregarding the nested proof structure.

 ML bindings introduced by 'ML_prf' are discarded at the end of the

 proof.  (Requires Poly/ML 5.2 or later.)

 and Method.setup, as well as commands 'attribute_setup' and

 and Method.setup, as well as Isar commands 'attribute_setup' and

 * ML bindings produced via Isar commands are stored within the Isar

 * Simplified interface for defining document antiquotations via

 context (theory or proof).  Consequently, commands like 'use' and 'ML'

 ThyOutput.antiquotation, ThyOutput.output, and optionally

 become thread-safe and work with undo as expected (concerning

 ThyOutput.maybe_pretty_source.  INCOMPATIBILITY, need to simplify user

 top-level bindings, not side-effects on global references).

 antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common

 INCOMPATIBILITY, need to provide proper Isar context when invoking the

 examples.

 compiler at runtime; really global bindings need to be given outside a

 theory. [Poly/ML 5.2 or later]

 * Command 'ML_prf' is analogous to 'ML' but works within a proof

 context. Top-level ML bindings are stored within the proof context in

 a purely sequential fashion, disregarding the nested proof structure.

 ML bindings introduced by 'ML_prf' are discarded at the end of the

 proof.  [Poly/ML 5.2 or later]

 * Generic Toplevel.add_hook interface allows to analyze the result of

 transactions.  E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML

 for theorem dependency output of transactions resulting in a new

 theory state.

 qualification (by packages and local theory targets), as well as

 qualification by packages and local theory targets, as well as proper

 proper tracking of source positions.  INCOMPATIBILITY, need to wrap

 tracking of source positions.  INCOMPATIBILITY, need to wrap old

 old bstring values into Binding.name, or better pass through abstract

 bstring values into Binding.name, or better pass through abstract

 * Antiquotations: block-structured compilation context indicated by

 * Rules and tactics that read instantiations (read_instantiate,

 res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof

 context, which is required for parsing and type-checking.  Moreover,

 the variables are specified as plain indexnames, not string encodings

 thereof.  INCOMPATIBILITY.

 * Generic Toplevel.add_hook interface allows to analyze the result of

 transactions.  E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML

 for theorem dependency output of transactions resulting in a new

 theory state.

 * ML antiquotations: block-structured compilation context indicated by

 * Status messages (with exact source position information) are

 * Added homegrown Isabelle font with unicode layout, see lib/fonts.

 * Various status messages (with exact source position information) are