Isabelle NEWS -- history user-relevant changes

 ==============================================

 New in this Isabelle version

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

 *** General ***

 * System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER

 (and thus refers to something like $HOME/.isabelle/IsabelleXXXX),

 while the default heap location within that directory lacks that extra

 suffix.  This isolates multiple Isabelle installations from each

 other, avoiding problems with old settings in new versions.

 INCOMPATIBILITY, need to copy/upgrade old user settings manually.

 * Significantly improved Isabelle/Isar implementation manual.

 * Explicit treatment of UTF8 sequences as Isabelle symbols, such that

 a Unicode character is treated as a single symbol, not a sequence of

 non-ASCII bytes as before.  Since Isabelle/ML string literals may

 contain symbols without further backslash escapes, Unicode can now be

 used here as well.  Recall that Symbol.explode in ML provides a

 consistent view on symbols, while raw explode (or String.explode)

 merely give a byte-oriented representation.

 * Theory loading: only the master source file is looked-up in the

 implicit load path, all other files are addressed relatively to its

 directory.  Minor INCOMPATIBILITY, subtle change in semantics.

 * Special treatment of ML file names has been discontinued.

 Historically, optional extensions .ML or .sml were added on demand --

 at the cost of clarity of file dependencies.  Recall that Isabelle/ML

 files exclusively use the .ML extension.  Minor INCOMPATIBILTY.

 * Various options that affect pretty printing etc. are now properly

 handled within the context via configuration options, instead of

 unsynchronized references.  There are both ML Config.T entities and

 Isar declaration attributes to access these.

   ML (Config.T)                 Isar (attribute)

   eta_contract                  eta_contract

   show_brackets                 show_brackets

   show_sorts                    show_sorts

   show_types                    show_types

   show_question_marks           show_question_marks

   show_consts                   show_consts

   Syntax.ambiguity_level        syntax_ambiguity_level

   Goal_Display.goals_limit      goals_limit

   Goal_Display.show_main_goal   show_main_goal

   Thy_Output.display            thy_output_display

   Thy_Output.quotes             thy_output_quotes

   Thy_Output.indent             thy_output_indent

   Thy_Output.source             thy_output_source

   Thy_Output.break              thy_output_break

 Note that corresponding "..._default" references in ML may be only

 changed globally at the ROOT session setup, but *not* within a theory.

 *** Pure ***

 * Support for real valued configuration options, using simplistic

 floating-point notation that coincides with the inner syntax for

 float_token.

 * Support for real valued preferences (with approximative PGIP type).

 * Interpretation command 'interpret' accepts a list of equations like

 'interpretation' does.

 * Diagnostic command 'print_interps' prints interpretations in proofs

 in addition to interpretations in theories.

 * Discontinued obsolete 'global' and 'local' commands to manipulate

 the theory name space.  Rare INCOMPATIBILITY.  The ML functions

 Sign.root_path and Sign.local_path may be applied directly where this

 feature is still required for historical reasons.

 * Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use

 'definition' instead.

 * Document antiquotations @{class} and @{type} print classes and type

 constructors.

 * Document antiquotation @{file} checks file/directory entries within

 the local file system.

 *** HOL ***

 * Code generator: globbing constant expressions "*" and "Theory.*" have been

 replaced by the more idiomatic "_" and "Theory._".  INCOMPATIBILITY.

 * Theory Enum (for explicit enumerations of finite types) is now part of

 the HOL-Main image. INCOMPATIBILITY: All constants of the Enum theory now 

 have to be referred to by its qualified name.

   constants

     enum -> Enum.enum

     nlists -> Enum.nlists

     product -> Enum.product

 * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to

 avoid confusion with finite sets.  INCOMPATIBILITY.

 * Quickcheck's generator for random generation is renamed from "code" to

 "random".  INCOMPATIBILITY.

 * Theory Multiset provides stable quicksort implementation of sort_key.

 * Quickcheck now has a configurable time limit which is set to 30 seconds

 by default. This can be changed by adding [timeout = n] to the quickcheck

 command. The time limit for Auto Quickcheck is still set independently.

 * New command 'partial_function' provides basic support for recursive

 function definitions over complete partial orders. Concrete instances

 are provided for i) the option type, ii) tail recursion on arbitrary

 types, and iii) the heap monad of Imperative_HOL. See

 HOL/ex/Fundefs.thy and HOL/Imperative_HOL/ex/Linked_Lists.thy for

 examples.

 * Predicates `distinct` and `sorted` now defined inductively, with nice

 induction rules.  INCOMPATIBILITY: former distinct.simps and sorted.simps

 now named distinct_simps and sorted_simps.

 * Constant `contents` renamed to `the_elem`, to free the generic name

 contents for other uses.  INCOMPATIBILITY.

 * Dropped syntax for old primrec package.  INCOMPATIBILITY.

 * Improved infrastructure for term evaluation using code generator

 techniques, in particular static evaluation conversions.

 * String.literal is a type, but not a datatype.  INCOMPATIBILITY.

 * Renamed lemmas:

   expand_fun_eq -> fun_eq_iff

   expand_set_eq -> set_eq_iff

   set_ext -> set_eqI

  INCOMPATIBILITY.

 * Renamed lemma list: nat_number -> eval_nat_numeral

 * Renamed class eq and constant eq (for code generation) to class equal

 and constant equal, plus renaming of related facts and various tuning.

 INCOMPATIBILITY.

 * Scala (2.8 or higher) has been added to the target languages of

 the code generator.

 * Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.

 * Removed output syntax "'a ~=> 'b" for "'a => 'b option". INCOMPATIBILITY.

 * Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;

 canonical names for instance definitions for functions; various improvements.

 INCOMPATIBILITY.

 * Records: logical foundation type for records do not carry a '_type' suffix

 any longer.  INCOMPATIBILITY.

 * Code generation for records: more idiomatic representation of record types.

 Warning: records are not covered by ancient SML code generation any longer.

 INCOMPATIBILITY.  In cases of need, a suitable rep_datatype declaration

 helps to succeed then:

   record 'a foo = ...

   ...

   rep_datatype foo_ext ...

 * Session Imperative_HOL: revamped, corrected dozens of inadequacies.

 INCOMPATIBILITY.

 * Quickcheck in locales considers interpretations of that locale for

 counter example search.

 * Theory Library/Monad_Syntax provides do-syntax for monad types.  Syntax

 in Library/State_Monad has been changed to avoid ambiguities.

 INCOMPATIBILITY.

 * Code generator: export_code without explicit file declaration prints

 to standard output.  INCOMPATIBILITY.

 * Abolished symbol type names:  "prod" and "sum" replace "*" and "+"

 respectively.  INCOMPATIBILITY.

 * Name "Plus" of disjoint sum operator "<+>" is now hidden.

   Write Sum_Type.Plus.

 * Constant "split" has been merged with constant "prod_case";  names

 of ML functions, facts etc. involving split have been retained so far,

 though.  INCOMPATIBILITY.

 * Dropped old infix syntax "mem" for List.member;  use "in set"

 instead.  INCOMPATIBILITY.

 * Refactoring of code-generation specific operations in List.thy

   constants

     null ~> List.null

   facts

     mem_iff ~> member_def

     null_empty ~> null_def

 INCOMPATIBILITY.  Note that these were not suppossed to be used

 regularly unless for striking reasons;  their main purpose was code

 generation.

 * Some previously unqualified names have been qualified:

   types

     bool ~> HOL.bool

     nat ~> Nat.nat

   constants

     Trueprop ~> HOL.Trueprop

     True ~> HOL.True

     False ~> HOL.False

     op & ~> HOL.conj

     op | ~> HOL.disj

     op --> ~> HOL.implies

     op = ~> HOL.eq

     Not ~> HOL.Not

     The ~> HOL.The

     All ~> HOL.All

     Ex ~> HOL.Ex

     Ex1 ~> HOL.Ex1

     Let ~> HOL.Let

     If ~> HOL.If

     Ball ~> Set.Ball

     Bex ~> Set.Bex

     Suc ~> Nat.Suc

     Pair ~> Product_Type.Pair

     fst ~> Product_Type.fst

     snd ~> Product_Type.snd

     curry ~> Product_Type.curry

     op : ~> Set.member

     Collect ~> Set.Collect

 INCOMPATIBILITY.

 * Removed simplifier congruence rule of "prod_case", as has for long

 been the case with "split".  INCOMPATIBILITY.

 * Datatype package: theorems generated for executable equality

 (class eq) carry proper names and are treated as default code

 equations.

 * Removed lemma Option.is_none_none (Duplicate of is_none_def).

 INCOMPATIBILITY.

 * List.thy: use various operations from the Haskell prelude when

 generating Haskell code.

 * Multiset.thy: renamed empty_idemp -> empty_neutral

 * code_simp.ML and method code_simp: simplification with rules determined

 by code generator.

 * code generator: do not print function definitions for case

 combinators any longer.

 * Multivariate Analysis: Introduced a type class for euclidean space. Most

 theorems are now stated in terms of euclidean spaces instead of finite

 cartesian products.

   types

     real ^ 'n ~>  'a::real_vector

               ~>  'a::euclidean_space

               ~>  'a::ordered_euclidean_space

         (depends on your needs)

   constants

      _ $ _        ~> _ $$ _

      \<chi> x. _  ~> \<chi>\<chi> x. _

      CARD('n)     ~> DIM('a)

 Also note that the indices are now natural numbers and not from some finite

 type. Finite cartesian products of euclidean spaces, products of euclidean

 spaces the real and complex numbers are instantiated to be euclidean_spaces.

 INCOMPATIBILITY.

 * Probability: Introduced pinfreal as real numbers with infinity. Use pinfreal

 as value for measures. Introduces Lebesgue Measure based on the integral in

 Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure

 spaces.

  INCOMPATIBILITY.

 * Inductive package: offers new command "inductive_simps" to automatically

 derive instantiated and simplified equations for inductive predicates,

 similar to inductive_cases.

 * "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f"

 is now an abbreviation of "range f = UNIV". The theorems bij_def and

 surj_def are unchanged.  INCOMPATIBILITY.

 * Function package: .psimps rules are no longer implicitly declared [simp].

 INCOMPATIBILITY.

 * Weaker versions of the "meson" and "metis" proof methods are now available in

   "HOL-Plain", without dependency on "Hilbert_Choice". The proof methods become

   more powerful after "Hilbert_Choice" is loaded in "HOL-Main".

 * MESON: Renamed lemmas:

   meson_not_conjD ~> Meson.not_conjD

   meson_not_disjD ~> Meson.not_disjD

   meson_not_notD ~> Meson.not_notD

   meson_not_allD ~> Meson.not_allD

   meson_not_exD ~> Meson.not_exD

   meson_imp_to_disjD ~> Meson.imp_to_disjD

   meson_not_impD ~> Meson.not_impD

   meson_iff_to_disjD ~> Meson.iff_to_disjD

   meson_not_iffD ~> Meson.not_iffD

   meson_not_refl_disj_D ~> Meson.not_refl_disj_D

   meson_conj_exD1 ~> Meson.conj_exD1

   meson_conj_exD2 ~> Meson.conj_exD2

   meson_disj_exD ~> Meson.disj_exD

   meson_disj_exD1 ~> Meson.disj_exD1

   meson_disj_exD2 ~> Meson.disj_exD2

   meson_disj_assoc ~> Meson.disj_assoc

   meson_disj_comm ~> Meson.disj_comm

   meson_disj_FalseD1 ~> Meson.disj_FalseD1

   meson_disj_FalseD2 ~> Meson.disj_FalseD2

 INCOMPATIBILITY.

 * Auto Solve: Renamed "Auto Solve Direct". The tool is now available manually as

   "solve_direct".

 * Sledgehammer:

   - Added "smt" and "remote_smt" provers based on the "smt" proof method. See

     the Sledgehammer manual for details ("isabelle doc sledgehammer").

   - Renamed lemmas:

     COMBI_def ~> Meson.COMBI_def

     COMBK_def ~> Meson.COMBK_def

     COMBB_def ~> Meson.COMBB_def

     COMBC_def ~> Meson.COMBC_def

     COMBS_def ~> Meson.COMBS_def

     abs_I ~> Meson.abs_I

     abs_K ~> Meson.abs_K

     abs_B ~> Meson.abs_B

     abs_C ~> Meson.abs_C

     abs_S ~> Meson.abs_S

     INCOMPATIBILITY.

   - Renamed commands:

     sledgehammer atp_info ~> sledgehammer running_provers

     sledgehammer atp_kill ~> sledgehammer kill_provers

     sledgehammer available_atps ~> sledgehammer available_provers

     INCOMPATIBILITY.

   - Renamed options:

     sledgehammer [atps = ...] ~> sledgehammer [provers = ...]

     sledgehammer [atp = ...] ~> sledgehammer [prover = ...]

     sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77]

     (and "ms" and "min" are no longer supported)

     INCOMPATIBILITY.

 * Metis and Meson now have configuration options "meson_trace", "metis_trace",

   and "metis_verbose" that can be enabled to diagnose these tools. E.g.

     using [[metis_trace = true]]

 * Nitpick:

   - Renamed options:

     nitpick [timeout = 77 s] ~> nitpick [timeout = 77]

     nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]

     INCOMPATIBILITY.

   - Now requires Kodkodi 1.2.9. INCOMPATIBILITY.

   - Added support for partial quotient types.

   - Added local versions of the "Nitpick.register_xxx" functions.

   - Added "whack" option.

   - Allow registration of quotient types as codatatypes.

   - Improved "merge_type_vars" option to merge more types.

   - Removed unsound "fast_descrs" option.

   - Added custom symmetry breaking for datatypes, making it possible to reach

     higher cardinalities.

   - Prevent the expansion of too large definitions.

 * Changed SMT configuration options:

   - Renamed:

     z3_proofs ~> smt_oracle (with swapped semantics)

     z3_trace_assms ~> smt_trace_used_facts

     INCOMPATIBILITY.

   - Added:

     smt_verbose

     smt_datatypes

     cvc3_options

     yices_options

 * Boogie output files (.b2i files) need to be declared in the

 theory header.

 * Removed [split_format ... and ... and ...] version of

 [split_format].  Potential INCOMPATIBILITY.

 *** HOLCF ***

 * The domain package now runs in definitional mode by default: The

 former command 'new_domain' is now called 'domain'. To use the domain

 package in its original axiomatic mode, use 'domain (unsafe)'.

 INCOMPATIBILITY.

 * The new class 'domain' is now the default sort; the definitional

 domain package and the powerdomain theories both require this class.

 The new class 'predomain' is an unpointed version of 'domain'.

 Theories can be updated by replacing sort annotations as shown below.

 INCOMPATIBILITY.

   'a::type ~> 'a::countable

   'a::cpo  ~> 'a::predomain

   'a::pcpo ~> 'a::domain

 * The old type class 'rep' has been superseded by class 'domain'.

 Accordingly, users of the definitional package must remove any

 'default_sort rep' declarations. INCOMPATIBILITY.

 * The old type classes 'profinite' and 'bifinite', along with the

 overloaded constant 'approx' have been removed. INCOMPATIBILITY.

 * The type 'udom alg_defl' has been replaced by the non-parameterized

 type 'defl'. HOLCF no longer defines an embedding of type defl into

 udom by default; the instance proof defl :: domain is now available in

 HOLCF/Library/Defl_Bifinite.thy.

 * The syntax 'REP('a)' has been replaced with 'DEFL('a)'.

 * The predicate 'directed' has been removed. INCOMPATIBILITY.

 * The type class 'finite_po' has been removed. INCOMPATIBILITY.

 * Renamed some theorems (the original names are also still available).

   expand_fun_below   ~> fun_below_iff

   below_fun_ext      ~> fun_belowI

   expand_cfun_eq     ~> cfun_eq_iff

   ext_cfun           ~> cfun_eqI

   expand_cfun_below  ~> cfun_below_iff

   below_cfun_ext     ~> cfun_belowI

   cont2cont_Rep_CFun ~> cont2cont_APP

 * The Abs and Rep functions for various types have changed names.

 Related theorem names have also changed to match. INCOMPATIBILITY. 

   Rep_CFun  ~> Rep_cfun

   Abs_CFun  ~> Abs_cfun

   Rep_Sprod ~> Rep_sprod

   Abs_Sprod ~> Abs_sprod

   Rep_Ssum  ~> Rep_ssum

   Abs_Ssum  ~> Abs_ssum

 * Lemmas with names of the form *_defined_iff or *_strict_iff have

 been renamed to *_bottom_iff. INCOMPATIBILITY.

 * Various changes to bisimulation/coinduction with domain package:

   - Definitions of 'bisim' constants no longer mention definedness.

   - With mutual recursion, 'bisim' predicate is now curried.

   - With mutual recursion, each type gets a separate coind theorem.

   - Variable names in bisim_def and coinduct rules have changed.

 INCOMPATIBILITY.

 * Case combinators generated by the domain package for type 'foo'

 are now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.

 * Several theorems have been renamed to more accurately reflect the

 names of constants and types involved. INCOMPATIBILITY.

   thelub_const    ~> lub_const

   lub_const       ~> is_lub_const

   thelubI         ~> lub_eqI

   is_lub_lub      ~> is_lubD2

   lubI            ~> is_lub_lub

   unique_lub      ~> is_lub_unique

   is_ub_lub       ~> is_lub_rangeD1

   lub_bin_chain   ~> is_lub_bin_chain

   thelub_Pair     ~> lub_Pair

   lub_cprod       ~> is_lub_prod

   thelub_cprod    ~> lub_prod

   minimal_cprod   ~> minimal_prod

   inst_cprod_pcpo ~> inst_prod_pcpo

 * Many legacy theorem names have been discontinued. INCOMPATIBILITY.

   sq_ord_less_eq_trans ~> below_eq_trans

   sq_ord_eq_less_trans ~> eq_below_trans

   refl_less            ~> below_refl

   trans_less           ~> below_trans

   antisym_less         ~> below_antisym

   antisym_less_inverse ~> po_eq_conv [THEN iffD1]

   box_less             ~> box_below

   rev_trans_less       ~> rev_below_trans

   not_less2not_eq      ~> not_below2not_eq

   less_UU_iff          ~> below_UU_iff

   flat_less_iff        ~> flat_below_iff

   adm_less             ~> adm_below

   adm_not_less         ~> adm_not_below

   adm_compact_not_less ~> adm_compact_not_below

   less_fun_def         ~> below_fun_def

   expand_fun_less      ~> fun_below_iff

   less_fun_ext         ~> fun_belowI

   less_discr_def       ~> below_discr_def

   discr_less_eq        ~> discr_below_eq

   less_unit_def        ~> below_unit_def

   less_cprod_def       ~> below_prod_def

   prod_lessI           ~> prod_belowI

   Pair_less_iff        ~> Pair_below_iff

   fst_less_iff         ~> fst_below_iff

   snd_less_iff         ~> snd_below_iff

   expand_cfun_less     ~> cfun_below_iff

   less_cfun_ext        ~> cfun_belowI

   injection_less       ~> injection_below

   less_up_def          ~> below_up_def

   not_Iup_less         ~> not_Iup_below

   Iup_less             ~> Iup_below

   up_less              ~> up_below

   Def_inject_less_eq   ~> Def_below_Def

   Def_less_is_eq       ~> Def_below_iff

   spair_less_iff       ~> spair_below_iff

   less_sprod           ~> below_sprod

   spair_less           ~> spair_below

   sfst_less_iff        ~> sfst_below_iff

   ssnd_less_iff        ~> ssnd_below_iff

   fix_least_less       ~> fix_least_below

   dist_less_one        ~> dist_below_one

   less_ONE             ~> below_ONE

   ONE_less_iff         ~> ONE_below_iff

   less_sinlD           ~> below_sinlD

   less_sinrD           ~> below_sinrD

 *** FOL ***

 * All constant names are now qualified.  INCOMPATIBILITY.

 *** ZF ***

 * All constant names are now qualified.  INCOMPATIBILITY.

 *** ML ***

 * Former exception Library.UnequalLengths now coincides with

 ListPair.UnequalLengths.

 * Renamed raw "explode" function to "raw_explode" to emphasize its

 meaning.  Note that internally to Isabelle, Symbol.explode is used in

 almost all situations.

 * Discontinued obsolete function sys_error and exception SYS_ERROR.

 See implementation manual for further details on exceptions in

 Isabelle/ML.

 * Antiquotation @{assert} inlines a function bool -> unit that raises

 Fail if the argument is false.  Due to inlining the source position of

 failed assertions is included in the error output.

 * Discontinued antiquotation @{theory_ref}, which is obsolete since ML

 text is in practice always evaluated with a stable theory checkpoint.

 Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.

 * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its

 meaning.

 * Renamed structure PureThy to Pure_Thy and moved most of its

 operations to structure Global_Theory, to emphasize that this is

 rarely-used global-only stuff.

 * Discontinued Output.debug.  Minor INCOMPATIBILITY, use plain writeln

 instead (or tracing for high-volume output).

 * Configuration option show_question_marks only affects regular pretty

 printing of types and terms, not raw Term.string_of_vname.

 * ML_Context.thm and ML_Context.thms are no longer pervasive.  Rare

 INCOMPATIBILITY, superseded by static antiquotations @{thm} and

 @{thms} for most purposes.

 * ML structure Unsynchronized never opened, not even in Isar

 interaction mode as before.  Old Unsynchronized.set etc. have been

 discontinued -- use plain := instead.  This should be *rare* anyway,

 since modern tools always work via official context data, notably

 configuration options.

 * ML antiquotations @{theory} and @{theory_ref} refer to named

 theories from the ancestry of the current context, not any accidental

 theory loader state as before.  Potential INCOMPATIBILITY, subtle

 change in semantics.

 * Parallel and asynchronous execution requires special care concerning

 interrupts.  Structure Exn provides some convenience functions that

 avoid working directly with raw Interrupt.  User code must not absorb

 interrupts -- intermediate handling (for cleanup etc.) needs to be

 followed by re-raising of the original exception.  Another common

 source of mistakes are "handle _" patterns, which make the meaning of

 the program subject to physical effects of the environment.

 *** System ***

 * Discontinued support for Poly/ML 5.0 and 5.1 versions.

 New in Isabelle2009-2 (June 2010)

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

 *** General ***

 * Authentic syntax for *all* logical entities (type classes, type

 constructors, term constants): provides simple and robust

 correspondence between formal entities and concrete syntax.  Within

 the parse tree / AST representations, "constants" are decorated by

 their category (class, type, const) and spelled out explicitly with

 their full internal name.

 Substantial INCOMPATIBILITY concerning low-level syntax declarations

 and translations (translation rules and translation functions in ML).

 Some hints on upgrading:

   - Many existing uses of 'syntax' and 'translations' can be replaced

     by more modern 'type_notation', 'notation' and 'abbreviation',

     which are independent of this issue.

   - 'translations' require markup within the AST; the term syntax

     provides the following special forms:

       CONST c   -- produces syntax version of constant c from context

       XCONST c  -- literally c, checked as constant from context

       c         -- literally c, if declared by 'syntax'

     Plain identifiers are treated as AST variables -- occasionally the

     system indicates accidental variables via the error "rhs contains

     extra variables".

     Type classes and type constructors are marked according to their

     concrete syntax.  Some old translations rules need to be written

     for the "type" category, using type constructor application

     instead of pseudo-term application of the default category

     "logic".

   - 'parse_translation' etc. in ML may use the following

     antiquotations:

       @{class_syntax c}   -- type class c within parse tree / AST

       @{term_syntax c}    -- type constructor c within parse tree / AST

       @{const_syntax c}   -- ML version of "CONST c" above

       @{syntax_const c}   -- literally c (checked wrt. 'syntax' declarations)

   - Literal types within 'typed_print_translations', i.e. those *not*

     represented as pseudo-terms are represented verbatim.  Use @{class

     c} or @{type_name c} here instead of the above syntax

     antiquotations.

 Note that old non-authentic syntax was based on unqualified base

 names, so all of the above "constant" names would coincide.  Recall

 that 'print_syntax' and ML_command "set Syntax.trace_ast" help to

 diagnose syntax problems.

 * Type constructors admit general mixfix syntax, not just infix.

 * Concrete syntax may be attached to local entities without a proof

 body, too.  This works via regular mixfix annotations for 'fix',

 'def', 'obtain' etc. or via the explicit 'write' command, which is

 similar to the 'notation' command in theory specifications.

 * Discontinued unnamed infix syntax (legacy feature for many years) --

 need to specify constant name and syntax separately.  Internal ML

 datatype constructors have been renamed from InfixName to Infix etc.

 Minor INCOMPATIBILITY.

 * Schematic theorem statements need to be explicitly markup as such,

 via commands 'schematic_lemma', 'schematic_theorem',

 'schematic_corollary'.  Thus the relevance of the proof is made

 syntactically clear, which impacts performance in a parallel or

 asynchronous interactive environment.  Minor INCOMPATIBILITY.

 * Use of cumulative prems via "!" in some proof methods has been

 discontinued (old legacy feature).

 * References 'trace_simp' and 'debug_simp' have been replaced by

 configuration options stored in the context. Enabling tracing (the

 case of debugging is similar) in proofs works via

   using [[trace_simp = true]]

 Tracing is then active for all invocations of the simplifier in

 subsequent goal refinement steps. Tracing may also still be enabled or

 disabled via the ProofGeneral settings menu.

 * Separate commands 'hide_class', 'hide_type', 'hide_const',

 'hide_fact' replace the former 'hide' KIND command.  Minor

 INCOMPATIBILITY.

 * Improved parallelism of proof term normalization: usedir -p2 -q0 is

 more efficient than combinations with -q1 or -q2.

 *** Pure ***

 * Proofterms record type-class reasoning explicitly, using the

 "unconstrain" operation internally.  This eliminates all sort

 constraints from a theorem and proof, introducing explicit

 OFCLASS-premises.  On the proof term level, this operation is

 automatically applied at theorem boundaries, such that closed proofs

 are always free of sort constraints.  INCOMPATIBILITY for tools that

 inspect proof terms.

 * Local theory specifications may depend on extra type variables that

 are not present in the result type -- arguments TYPE('a) :: 'a itself

 are added internally.  For example:

   definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"

 * Predicates of locales introduced by classes carry a mandatory

 "class" prefix.  INCOMPATIBILITY.

 * Vacuous class specifications observe default sort.  INCOMPATIBILITY.

 * Old 'axclass' command has been discontinued.  INCOMPATIBILITY, use

 'class' instead.

 * Command 'code_reflect' allows to incorporate generated ML code into

 runtime environment; replaces immature code_datatype antiquotation.

 INCOMPATIBILITY.

 * Code generator: simple concept for abstract datatypes obeying

 invariants.

 * Code generator: details of internal data cache have no impact on the

 user space functionality any longer.

 * Methods "unfold_locales" and "intro_locales" ignore non-locale

 subgoals.  This is more appropriate for interpretations with 'where'.

 INCOMPATIBILITY.

 * Command 'example_proof' opens an empty proof body.  This allows to

 experiment with Isar, without producing any persistent result.

 * Commands 'type_notation' and 'no_type_notation' declare type syntax

 within a local theory context, with explicit checking of the

 constructors involved (in contrast to the raw 'syntax' versions).

 * Commands 'types' and 'typedecl' now work within a local theory

 context -- without introducing dependencies on parameters or

 assumptions, which is not possible in Isabelle/Pure.

 * Command 'defaultsort' has been renamed to 'default_sort', it works

 within a local theory context.  Minor INCOMPATIBILITY.

 *** HOL ***

 * Command 'typedef' now works within a local theory context -- without

 introducing dependencies on parameters or assumptions, which is not

 possible in Isabelle/Pure/HOL.  Note that the logical environment may

 contain multiple interpretations of local typedefs (with different

 non-emptiness proofs), even in a global theory context.

 * New package for quotient types.  Commands 'quotient_type' and

 'quotient_definition' may be used for defining types and constants by

 quotient constructions.  An example is the type of integers created by

 quotienting pairs of natural numbers:

   fun

     intrel :: "(nat * nat) => (nat * nat) => bool"

   where

     "intrel (x, y) (u, v) = (x + v = u + y)"

   quotient_type int = "nat * nat" / intrel

     by (auto simp add: equivp_def expand_fun_eq)

   quotient_definition

     "0::int" is "(0::nat, 0::nat)"

 The method "lifting" can be used to lift of theorems from the

 underlying "raw" type to the quotient type.  The example

 src/HOL/Quotient_Examples/FSet.thy includes such a quotient

 construction and provides a reasoning infrastructure for finite sets.

 * Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid

 clash with new theory Quotient in Main HOL.

 * Moved the SMT binding into the main HOL session, eliminating

 separate HOL-SMT session.

 * List membership infix mem operation is only an input abbreviation.

 INCOMPATIBILITY.

 * Theory Library/Word.thy has been removed.  Use library Word/Word.thy

 for future developements; former Library/Word.thy is still present in

 the AFP entry RSAPPS.

 * Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no

 longer shadowed.  INCOMPATIBILITY.

 * Dropped theorem duplicate comp_arith; use semiring_norm instead.

 INCOMPATIBILITY.

 * Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.

 INCOMPATIBILITY.

 * Dropped normalizing_semiring etc; use the facts in semiring classes

 instead.  INCOMPATIBILITY.

 * Dropped several real-specific versions of lemmas about floor and

 ceiling; use the generic lemmas from theory "Archimedean_Field"

 instead.  INCOMPATIBILITY.

   floor_number_of_eq         ~> floor_number_of

   le_floor_eq_number_of      ~> number_of_le_floor

   le_floor_eq_zero           ~> zero_le_floor

   le_floor_eq_one            ~> one_le_floor

   floor_less_eq_number_of    ~> floor_less_number_of

   floor_less_eq_zero         ~> floor_less_zero

   floor_less_eq_one          ~> floor_less_one

   less_floor_eq_number_of    ~> number_of_less_floor

   less_floor_eq_zero         ~> zero_less_floor

   less_floor_eq_one          ~> one_less_floor

   floor_le_eq_number_of      ~> floor_le_number_of

   floor_le_eq_zero           ~> floor_le_zero

   floor_le_eq_one            ~> floor_le_one

   floor_subtract_number_of   ~> floor_diff_number_of

   floor_subtract_one         ~> floor_diff_one

   ceiling_number_of_eq       ~> ceiling_number_of

   ceiling_le_eq_number_of    ~> ceiling_le_number_of

   ceiling_le_zero_eq         ~> ceiling_le_zero

   ceiling_le_eq_one          ~> ceiling_le_one

   less_ceiling_eq_number_of  ~> number_of_less_ceiling

   less_ceiling_eq_zero       ~> zero_less_ceiling

   less_ceiling_eq_one        ~> one_less_ceiling

   ceiling_less_eq_number_of  ~> ceiling_less_number_of

   ceiling_less_eq_zero       ~> ceiling_less_zero

   ceiling_less_eq_one        ~> ceiling_less_one

   le_ceiling_eq_number_of    ~> number_of_le_ceiling

   le_ceiling_eq_zero         ~> zero_le_ceiling

   le_ceiling_eq_one          ~> one_le_ceiling

   ceiling_subtract_number_of ~> ceiling_diff_number_of

   ceiling_subtract_one       ~> ceiling_diff_one

 * Theory "Finite_Set": various folding_XXX locales facilitate the

 application of the various fold combinators on finite sets.

 * Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"

 provides abstract red-black tree type which is backed by "RBT_Impl" as

 implementation.  INCOMPATIBILTY.

 * Theory Library/Coinductive_List has been removed -- superseded by

 AFP/thys/Coinductive.

 * Theory PReal, including the type "preal" and related operations, has

 been removed.  INCOMPATIBILITY.

 * Real: new development using Cauchy Sequences.

 * Split off theory "Big_Operators" containing setsum, setprod,

 Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.

 * Theory "Rational" renamed to "Rat", for consistency with "Nat",

 "Int" etc.  INCOMPATIBILITY.

 * Constant Rat.normalize needs to be qualified.  INCOMPATIBILITY.

 * New set of rules "ac_simps" provides combined assoc / commute

 rewrites for all interpretations of the appropriate generic locales.

 * Renamed theory "OrderedGroup" to "Groups" and split theory

 "Ring_and_Field" into theories "Rings" and "Fields"; for more

 appropriate and more consistent names suitable for name prefixes

 within the HOL theories.  INCOMPATIBILITY.

 * Some generic constants have been put to appropriate theories:

   - less_eq, less: Orderings

   - zero, one, plus, minus, uminus, times, abs, sgn: Groups

   - inverse, divide: Rings

 INCOMPATIBILITY.

 * More consistent naming of type classes involving orderings (and

 lattices):

     lower_semilattice                   ~> semilattice_inf

     upper_semilattice                   ~> semilattice_sup

     dense_linear_order                  ~> dense_linorder

     pordered_ab_group_add               ~> ordered_ab_group_add

     pordered_ab_group_add_abs           ~> ordered_ab_group_add_abs

     pordered_ab_semigroup_add           ~> ordered_ab_semigroup_add

     pordered_ab_semigroup_add_imp_le    ~> ordered_ab_semigroup_add_imp_le

     pordered_cancel_ab_semigroup_add    ~> ordered_cancel_ab_semigroup_add

     pordered_cancel_comm_semiring       ~> ordered_cancel_comm_semiring

     pordered_cancel_semiring            ~> ordered_cancel_semiring

     pordered_comm_monoid_add            ~> ordered_comm_monoid_add

     pordered_comm_ring                  ~> ordered_comm_ring

     pordered_comm_semiring              ~> ordered_comm_semiring

     pordered_ring                       ~> ordered_ring

     pordered_ring_abs                   ~> ordered_ring_abs

     pordered_semiring                   ~> ordered_semiring

     ordered_ab_group_add                ~> linordered_ab_group_add

     ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add

     ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add

     ordered_comm_semiring_strict        ~> linordered_comm_semiring_strict

     ordered_field                       ~> linordered_field

     ordered_field_no_lb                 ~> linordered_field_no_lb

     ordered_field_no_ub                 ~> linordered_field_no_ub

     ordered_field_dense_linear_order    ~> dense_linordered_field

     ordered_idom                        ~> linordered_idom

     ordered_ring                        ~> linordered_ring

     ordered_ring_le_cancel_factor       ~> linordered_ring_le_cancel_factor

     ordered_ring_less_cancel_factor     ~> linordered_ring_less_cancel_factor

     ordered_ring_strict                 ~> linordered_ring_strict

     ordered_semidom                     ~> linordered_semidom

     ordered_semiring                    ~> linordered_semiring

     ordered_semiring_1                  ~> linordered_semiring_1

     ordered_semiring_1_strict           ~> linordered_semiring_1_strict

     ordered_semiring_strict             ~> linordered_semiring_strict

   The following slightly odd type classes have been moved to a

   separate theory Library/Lattice_Algebras:

     lordered_ab_group_add               ~> lattice_ab_group_add

     lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs

     lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add

     lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add

     lordered_ring                       ~> lattice_ring

 INCOMPATIBILITY.

 * Refined field classes:

   - classes division_ring_inverse_zero, field_inverse_zero,

     linordered_field_inverse_zero include rule inverse 0 = 0 --

     subsumes former division_by_zero class;

   - numerous lemmas have been ported from field to division_ring.

 INCOMPATIBILITY.

 * Refined algebra theorem collections:

   - dropped theorem group group_simps, use algebra_simps instead;

   - dropped theorem group ring_simps, use field_simps instead;

   - proper theorem collection field_simps subsumes former theorem

     groups field_eq_simps and field_simps;

   - dropped lemma eq_minus_self_iff which is a duplicate for

     equal_neg_zero.

 INCOMPATIBILITY.

 * Theory Finite_Set and List: some lemmas have been generalized from

 sets to lattices:

   fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf

   fun_left_comm_idem_union      ~> fun_left_comm_idem_sup

   inter_Inter_fold_inter        ~> inf_Inf_fold_inf

   union_Union_fold_union        ~> sup_Sup_fold_sup

   Inter_fold_inter              ~> Inf_fold_inf

   Union_fold_union              ~> Sup_fold_sup

   inter_INTER_fold_inter        ~> inf_INFI_fold_inf

   union_UNION_fold_union        ~> sup_SUPR_fold_sup

   INTER_fold_inter              ~> INFI_fold_inf

   UNION_fold_union              ~> SUPR_fold_sup

 * Theory "Complete_Lattice": lemmas top_def and bot_def have been

 replaced by the more convenient lemmas Inf_empty and Sup_empty.

 Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed

 by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace

 former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right

 subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.

 * Reorganized theory Multiset: swapped notation of pointwise and

 multiset order:

   - pointwise ordering is instance of class order with standard syntax

     <= and <;

   - multiset ordering has syntax <=# and <#; partial order properties

     are provided by means of interpretation with prefix

     multiset_order;

   - less duplication, less historical organization of sections,

     conversion from associations lists to multisets, rudimentary code

     generation;

   - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,

     if needed.

 Renamed:

   multiset_eq_conv_count_eq  ~>  multiset_ext_iff

   multi_count_ext  ~>  multiset_ext

   diff_union_inverse2  ~>  diff_union_cancelR

 INCOMPATIBILITY.

 * Theory Permutation: replaced local "remove" by List.remove1.

 * Code generation: ML and OCaml code is decorated with signatures.

 * Theory List: added transpose.

 * Library/Nat_Bijection.thy is a collection of bijective functions

 between nat and other types, which supersedes the older libraries

 Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy.  INCOMPATIBILITY.

   Constants:

   Nat_Int_Bij.nat2_to_nat         ~> prod_encode

   Nat_Int_Bij.nat_to_nat2         ~> prod_decode

   Nat_Int_Bij.int_to_nat_bij      ~> int_encode

   Nat_Int_Bij.nat_to_int_bij      ~> int_decode

   Countable.pair_encode           ~> prod_encode

   NatIso.prod2nat                 ~> prod_encode

   NatIso.nat2prod                 ~> prod_decode

   NatIso.sum2nat                  ~> sum_encode

   NatIso.nat2sum                  ~> sum_decode

   NatIso.list2nat                 ~> list_encode

   NatIso.nat2list                 ~> list_decode

   NatIso.set2nat                  ~> set_encode

   NatIso.nat2set                  ~> set_decode

   Lemmas:

   Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_decode

   Nat_Int_Bij.nat2_to_nat_inj     ~> inj_prod_encode

   Nat_Int_Bij.nat2_to_nat_surj    ~> surj_prod_encode

   Nat_Int_Bij.nat_to_nat2_inj     ~> inj_prod_decode

   Nat_Int_Bij.nat_to_nat2_surj    ~> surj_prod_decode

   Nat_Int_Bij.i2n_n2i_id          ~> int_encode_inverse

   Nat_Int_Bij.n2i_i2n_id          ~> int_decode_inverse

   Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode

   Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode

   Nat_Int_Bij.inj_nat_to_int_bij  ~> inj_int_encode

   Nat_Int_Bij.inj_int_to_nat_bij  ~> inj_int_decode

   Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode

   Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode

 * Sledgehammer:

   - Renamed ATP commands:

     atp_info     ~> sledgehammer running_atps

     atp_kill     ~> sledgehammer kill_atps

     atp_messages ~> sledgehammer messages

     atp_minimize ~> sledgehammer minimize

     print_atps   ~> sledgehammer available_atps

     INCOMPATIBILITY.

   - Added user's manual ("isabelle doc sledgehammer").

   - Added option syntax and "sledgehammer_params" to customize

     Sledgehammer's behavior.  See the manual for details.

   - Modified the Isar proof reconstruction code so that it produces

     direct proofs rather than proofs by contradiction.  (This feature

     is still experimental.)

   - Made Isar proof reconstruction work for SPASS, remote ATPs, and in

     full-typed mode.

   - Added support for TPTP syntax for SPASS via the "spass_tptp" ATP.

 * Nitpick:

   - Added and implemented "binary_ints" and "bits" options.

   - Added "std" option and implemented support for nonstandard models.

   - Added and implemented "finitize" option to improve the precision

     of infinite datatypes based on a monotonicity analysis.

   - Added support for quotient types.

   - Added support for "specification" and "ax_specification"

     constructs.

   - Added support for local definitions (for "function" and

     "termination" proofs).

   - Added support for term postprocessors.

   - Optimized "Multiset.multiset" and "FinFun.finfun".

   - Improved efficiency of "destroy_constrs" optimization.

   - Fixed soundness bugs related to "destroy_constrs" optimization and

     record getters.

   - Fixed soundness bug related to higher-order constructors.

   - Fixed soundness bug when "full_descrs" is enabled.

   - Improved precision of set constructs.

   - Added "atoms" option.

   - Added cache to speed up repeated Kodkod invocations on the same

     problems.

   - Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and

     "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and

     "SAT4J_Light".  INCOMPATIBILITY.

   - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",

     "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.

   - Removed "nitpick_intro" attribute.  INCOMPATIBILITY.

 * Method "induct" now takes instantiations of the form t, where t is not

   a variable, as a shorthand for "x == t", where x is a fresh variable.

   If this is not intended, t has to be enclosed in parentheses.

   By default, the equalities generated by definitional instantiations

   are pre-simplified, which may cause parameters of inductive cases

   to disappear, or may even delete some of the inductive cases.

   Use "induct (no_simp)" instead of "induct" to restore the old

   behaviour. The (no_simp) option is also understood by the "cases"

   and "nominal_induct" methods, which now perform pre-simplification, too.

   INCOMPATIBILITY.

 *** HOLCF ***

 * Variable names in lemmas generated by the domain package have

 changed; the naming scheme is now consistent with the HOL datatype

 package.  Some proof scripts may be affected, INCOMPATIBILITY.

 * The domain package no longer defines the function "foo_copy" for

 recursive domain "foo".  The reach lemma is now stated directly in

 terms of "foo_take".  Lemmas and proofs that mention "foo_copy" must

 be reformulated in terms of "foo_take", INCOMPATIBILITY.

 * Most definedness lemmas generated by the domain package (previously

 of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form

 like "foo$x = UU <-> x = UU", which works better as a simp rule.

 Proofs that used definedness lemmas as intro rules may break,

 potential INCOMPATIBILITY.

 * Induction and casedist rules generated by the domain package now

 declare proper case_names (one called "bottom", and one named for each

 constructor).  INCOMPATIBILITY.

 * For mutually-recursive domains, separate "reach" and "take_lemma"

 rules are generated for each domain, INCOMPATIBILITY.

   foo_bar.reach       ~> foo.reach  bar.reach

   foo_bar.take_lemmas ~> foo.take_lemma  bar.take_lemma

 * Some lemmas generated by the domain package have been renamed for

 consistency with the datatype package, INCOMPATIBILITY.

   foo.ind        ~> foo.induct

   foo.finite_ind ~> foo.finite_induct

   foo.coind      ~> foo.coinduct

   foo.casedist   ~> foo.exhaust

   foo.exhaust    ~> foo.nchotomy

 * For consistency with other definition packages, the fixrec package

 now generates qualified theorem names, INCOMPATIBILITY.

   foo_simps  ~> foo.simps

   foo_unfold ~> foo.unfold

   foo_induct ~> foo.induct

 * The "fixrec_simp" attribute has been removed.  The "fixrec_simp"

 method and internal fixrec proofs now use the default simpset instead.

 INCOMPATIBILITY.

 * The "contlub" predicate has been removed.  Proof scripts should use

 lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.

 * The "admw" predicate has been removed, INCOMPATIBILITY.

 * The constants cpair, cfst, and csnd have been removed in favor of

 Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY.

 *** ML ***

 * Antiquotations for basic formal entities:

     @{class NAME}         -- type class

     @{class_syntax NAME}  -- syntax representation of the above

     @{type_name NAME}     -- logical type

     @{type_abbrev NAME}   -- type abbreviation

     @{nonterminal NAME}   -- type of concrete syntactic category

     @{type_syntax NAME}   -- syntax representation of any of the above

     @{const_name NAME}    -- logical constant (INCOMPATIBILITY)

     @{const_abbrev NAME}  -- abbreviated constant

     @{const_syntax NAME}  -- syntax representation of any of the above

 * Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw

 syntax constant (cf. 'syntax' command).

 * Antiquotation @{make_string} inlines a function to print arbitrary

 values similar to the ML toplevel.  The result is compiler dependent

 and may fall back on "?" in certain situations.

 * Diagnostic commands 'ML_val' and 'ML_command' may refer to

 antiquotations @{Isar.state} and @{Isar.goal}.  This replaces impure

 Isar.state() and Isar.goal(), which belong to the old TTY loop and do

 not work with the asynchronous Isar document model.

 * Configuration options now admit dynamic default values, depending on

 the context or even global references.

 * SHA1.digest digests strings according to SHA-1 (see RFC 3174).  It

 uses an efficient external library if available (for Poly/ML).

 * Renamed some important ML structures, while keeping the old names

 for some time as aliases within the structure Legacy:

   OuterKeyword  ~>  Keyword

   OuterLex      ~>  Token

   OuterParse    ~>  Parse

   OuterSyntax   ~>  Outer_Syntax

   PrintMode     ~>  Print_Mode

   SpecParse     ~>  Parse_Spec

   ThyInfo       ~>  Thy_Info

   ThyLoad       ~>  Thy_Load

   ThyOutput     ~>  Thy_Output

   TypeInfer     ~>  Type_Infer

 Note that "open Legacy" simplifies porting of sources, but forgetting

 to remove it again will complicate porting again in the future.

 * Most operations that refer to a global context are named

 accordingly, e.g. Simplifier.global_context or

 ProofContext.init_global.  There are some situations where a global

 context actually works, but under normal circumstances one needs to

 pass the proper local context through the code!

 * Discontinued old TheoryDataFun with its copy/init operation -- data

 needs to be pure.  Functor Theory_Data_PP retains the traditional

 Pretty.pp argument to merge, which is absent in the standard

 Theory_Data version.

 * Sorts.certify_sort and derived "cert" operations for types and terms

 no longer minimize sorts.  Thus certification at the boundary of the

 inference kernel becomes invariant under addition of class relations,

 which is an important monotonicity principle.  Sorts are now minimized

 in the syntax layer only, at the boundary between the end-user and the

 system.  Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort

 explicitly in rare situations.

 * Renamed old-style Drule.standard to Drule.export_without_context, to

 emphasize that this is in no way a standard operation.

 INCOMPATIBILITY.

 * Subgoal.FOCUS (and variants): resulting goal state is normalized as

 usual for resolution.  Rare INCOMPATIBILITY.

 * Renamed varify/unvarify operations to varify_global/unvarify_global

 to emphasize that these only work in a global situation (which is

 quite rare).

 * Curried take and drop in library.ML; negative length is interpreted

 as infinity (as in chop).  Subtle INCOMPATIBILITY.

 * Proof terms: type substitutions on proof constants now use canonical

 order of type variables.  INCOMPATIBILITY for tools working with proof

 terms.

 * Raw axioms/defs may no longer carry sort constraints, and raw defs

 may no longer carry premises.  User-level specifications are

 transformed accordingly by Thm.add_axiom/add_def.

 *** System ***

 * Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;

 ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions.  Note that

 proof terms are enabled unconditionally in the new HOL-Proofs image.

 * Discontinued old ISABELLE and ISATOOL environment settings (legacy

 feature since Isabelle2009).  Use ISABELLE_PROCESS and ISABELLE_TOOL,

 respectively.

 * Old lib/scripts/polyml-platform is superseded by the

 ISABELLE_PLATFORM setting variable, which defaults to the 32 bit

 variant, even on a 64 bit machine.  The following example setting

 prefers 64 bit if available:

   ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"

 * The preliminary Isabelle/jEdit application demonstrates the emerging

 Isabelle/Scala layer for advanced prover interaction and integration.

 See src/Tools/jEdit or "isabelle jedit" provided by the properly built

 component.

 * "IsabelleText" is a Unicode font derived from Bitstream Vera Mono

 and Bluesky TeX fonts.  It provides the usual Isabelle symbols,

 similar to the default assignment of the document preparation system

 (cf. isabellesym.sty).  The Isabelle/Scala class Isabelle_System

 provides some operations for direct access to the font without asking

 the user for manual installation.

 New in Isabelle2009-1 (December 2009)

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

 *** General ***

 * Discontinued old form of "escaped symbols" such as \\<forall>.  Only

 one backslash should be used, even in ML sources.

 *** Pure ***

 * Locale interpretation propagates mixins along the locale hierarchy.

 The currently only available mixins are the equations used to map

 local definitions to terms of the target domain of an interpretation.

 * Reactivated diagnostic command 'print_interps'.  Use "print_interps

 loc" to print all interpretations of locale "loc" in the theory.

 Interpretations in proofs are not shown.

 * Thoroughly revised locales tutorial.  New section on conditional

 interpretation.

 * On instantiation of classes, remaining undefined class parameters

 are formally declared.  INCOMPATIBILITY.

 *** Document preparation ***

 * New generalized style concept for printing terms: @{foo (style) ...}

 instead of @{foo_style style ...}  (old form is still retained for

 backward compatibility).  Styles can be also applied for

 antiquotations prop, term_type and typeof.

 *** HOL ***

 * New proof method "smt" for a combination of first-order logic with

 equality, linear and nonlinear (natural/integer/real) arithmetic, and

 fixed-size bitvectors; there is also basic support for higher-order

 features (esp. lambda abstractions).  It is an incomplete decision

 procedure based on external SMT solvers using the oracle mechanism;

 for the SMT solver Z3, this method is proof-producing.  Certificates

 are provided to avoid calling the external solvers solely for

 re-checking proofs.  Due to a remote SMT service there is no need for

 installing SMT solvers locally.  See src/HOL/SMT.

 * New commands to load and prove verification conditions generated by

 the Boogie program verifier or derived systems (e.g. the Verifying C

 Compiler (VCC) or Spec#).  See src/HOL/Boogie.

 * New counterexample generator tool 'nitpick' based on the Kodkod

 relational model finder.  See src/HOL/Tools/Nitpick and

 src/HOL/Nitpick_Examples.

 * New commands 'code_pred' and 'values' to invoke the predicate

 compiler and to enumerate values of inductive predicates.

 * A tabled implementation of the reflexive transitive closure.

 * New implementation of quickcheck uses generic code generator;

 default generators are provided for all suitable HOL types, records

 and datatypes.  Old quickcheck can be re-activated importing theory

 Library/SML_Quickcheck.

 * New testing tool Mirabelle for automated proof tools.  Applies

 several tools and tactics like sledgehammer, metis, or quickcheck, to

 every proof step in a theory.  To be used in batch mode via the

 "mirabelle" utility.

 * New proof method "sos" (sum of squares) for nonlinear real

 arithmetic (originally due to John Harison). It requires theory

 Library/Sum_Of_Squares.  It is not a complete decision procedure but

 works well in practice on quantifier-free real arithmetic with +, -,

 *, ^, =, <= and <, i.e. boolean combinations of equalities and

 inequalities between polynomials.  It makes use of external

 semidefinite programming solvers.  Method "sos" generates a

 certificate that can be pasted into the proof thus avoiding the need

 to call an external tool every time the proof is checked.  See

 src/HOL/Library/Sum_Of_Squares.

 * New method "linarith" invokes existing linear arithmetic decision

 procedure only.

 * New command 'atp_minimal' reduces result produced by Sledgehammer.

 * New Sledgehammer option "Full Types" in Proof General settings menu.

 Causes full type information to be output to the ATPs.  This slows

 ATPs down considerably but eliminates a source of unsound "proofs"

 that fail later.

 * New method "metisFT": A version of metis that uses full type

 information in order to avoid failures of proof reconstruction.

 * New evaluator "approximate" approximates an real valued term using

 the same method as the approximation method.

 * Method "approximate" now supports arithmetic expressions as

 boundaries of intervals and implements interval splitting and Taylor

 series expansion.

 * ML antiquotation @{code_datatype} inserts definition of a datatype

 generated by the code generator; e.g. see src/HOL/Predicate.thy.

 * New theory SupInf of the supremum and infimum operators for sets of

 reals.

 * New theory Probability, which contains a development of measure

 theory, eventually leading to Lebesgue integration and probability.

 * Extended Multivariate Analysis to include derivation and Brouwer's

 fixpoint theorem.

 * Reorganization of number theory, INCOMPATIBILITY:

   - new number theory development for nat and int, in theories Divides

     and GCD as well as in new session Number_Theory

   - some constants and facts now suffixed with _nat and _int

     accordingly

   - former session NumberTheory now named Old_Number_Theory, including

     theories Legacy_GCD and Primes (prefer Number_Theory if possible)

   - moved theory Pocklington from src/HOL/Library to

     src/HOL/Old_Number_Theory

 * Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and

 lcm of finite and infinite sets. It is shown that they form a complete

 lattice.

 * Class semiring_div requires superclass no_zero_divisors and proof of

 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,

 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been

 generalized to class semiring_div, subsuming former theorems

 zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and

 zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.

 INCOMPATIBILITY.

 * Refinements to lattice classes and sets:

   - less default intro/elim rules in locale variant, more default

     intro/elim rules in class variant: more uniformity

   - lemma ge_sup_conv renamed to le_sup_iff, in accordance with

     le_inf_iff

   - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and

     sup_aci)

   - renamed ACI to inf_sup_aci

   - new class "boolean_algebra"

   - class "complete_lattice" moved to separate theory

     "Complete_Lattice"; corresponding constants (and abbreviations)

     renamed and with authentic syntax:

     Set.Inf ~>    Complete_Lattice.Inf

     Set.Sup ~>    Complete_Lattice.Sup

     Set.INFI ~>   Complete_Lattice.INFI

     Set.SUPR ~>   Complete_Lattice.SUPR

     Set.Inter ~>  Complete_Lattice.Inter

     Set.Union ~>  Complete_Lattice.Union

     Set.INTER ~>  Complete_Lattice.INTER

     Set.UNION ~>  Complete_Lattice.UNION

   - authentic syntax for

     Set.Pow

     Set.image

   - mere abbreviations:

     Set.empty               (for bot)

     Set.UNIV                (for top)

     Set.inter               (for inf, formerly Set.Int)

     Set.union               (for sup, formerly Set.Un)

     Complete_Lattice.Inter  (for Inf)

     Complete_Lattice.Union  (for Sup)

     Complete_Lattice.INTER  (for INFI)

     Complete_Lattice.UNION  (for SUPR)

   - object-logic definitions as far as appropriate

 INCOMPATIBILITY.  Care is required when theorems Int_subset_iff or

 Un_subset_iff are explicitly deleted as default simp rules; then also

 their lattice counterparts le_inf_iff and le_sup_iff have to be

 deleted to achieve the desired effect.

 * Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp

 rules by default any longer; the same applies to min_max.inf_absorb1

 etc.  INCOMPATIBILITY.

 * Rules sup_Int_eq and sup_Un_eq are no longer declared as

 pred_set_conv by default.  INCOMPATIBILITY.

 * Power operations on relations and functions are now one dedicated

 constant "compow" with infix syntax "^^".  Power operation on

 multiplicative monoids retains syntax "^" and is now defined generic

 in class power.  INCOMPATIBILITY.

 * Relation composition "R O S" now has a more standard argument order:

 "R O S = {(x, z). EX y. (x, y) : R & (y, z) : S}".  INCOMPATIBILITY,

 rewrite propositions with "S O R" --> "R O S". Proofs may occasionally

 break, since the O_assoc rule was not rewritten like this.  Fix using

 O_assoc[symmetric].  The same applies to the curried version "R OO S".

 * Function "Inv" is renamed to "inv_into" and function "inv" is now an

 abbreviation for "inv_into UNIV".  Lemmas are renamed accordingly.

 INCOMPATIBILITY.

 * Most rules produced by inductive and datatype package have mandatory

 prefixes.  INCOMPATIBILITY.

 * Changed "DERIV_intros" to a dynamic fact, which can be augmented by

 the attribute of the same name.  Each of the theorems in the list

 DERIV_intros assumes composition with an additional function and

 matches a variable to the derivative, which has to be solved by the

 Simplifier.  Hence (auto intro!: DERIV_intros) computes the derivative

 of most elementary terms.  Former Maclauren.DERIV_tac and

 Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros).

 INCOMPATIBILITY.

 * Code generator attributes follow the usual underscore convention:

     code_unfold     replaces    code unfold

     code_post       replaces    code post

     etc.

   INCOMPATIBILITY.

 * Renamed methods:

     sizechange -> size_change

     induct_scheme -> induction_schema

   INCOMPATIBILITY.

 * Discontinued abbreviation "arbitrary" of constant "undefined".

 INCOMPATIBILITY, use "undefined" directly.

 * Renamed theorems:

     Suc_eq_add_numeral_1 -> Suc_eq_plus1

     Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left

     Suc_plus1 -> Suc_eq_plus1

     *anti_sym -> *antisym*

     vector_less_eq_def -> vector_le_def

   INCOMPATIBILITY.

 * Added theorem List.map_map as [simp].  Removed List.map_compose.

 INCOMPATIBILITY.

 * Removed predicate "M hassize n" (<--> card M = n & finite M).

 INCOMPATIBILITY.

 *** HOLCF ***

 * Theory Representable defines a class "rep" of domains that are

 representable (via an ep-pair) in the universal domain type "udom".

 Instances are provided for all type constructors defined in HOLCF.

 * The 'new_domain' command is a purely definitional version of the

 domain package, for representable domains.  Syntax is identical to the

 old domain package.  The 'new_domain' package also supports indirect

 recursion using previously-defined type constructors.  See

 src/HOLCF/ex/New_Domain.thy for examples.

 * Method "fixrec_simp" unfolds one step of a fixrec-defined constant

 on the left-hand side of an equation, and then performs

 simplification.  Rewriting is done using rules declared with the

 "fixrec_simp" attribute.  The "fixrec_simp" method is intended as a

 replacement for "fixpat"; see src/HOLCF/ex/Fixrec_ex.thy for examples.

 * The pattern-match compiler in 'fixrec' can now handle constructors

 with HOL function types.  Pattern-match combinators for the Pair

 constructor are pre-configured.

 * The 'fixrec' package now produces better fixed-point induction rules

 for mutually-recursive definitions:  Induction rules have conclusions

 of the form "P foo bar" instead of "P <foo, bar>".

 * The constant "sq_le" (with infix syntax "<<" or "\<sqsubseteq>") has

 been renamed to "below".  The name "below" now replaces "less" in many

 theorem names.  (Legacy theorem names using "less" are still supported

 as well.)

 * The 'fixrec' package now supports "bottom patterns".  Bottom

 patterns can be used to generate strictness rules, or to make

 functions more strict (much like the bang-patterns supported by the

 Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for

 examples.

 *** ML ***

 * Support for Poly/ML 5.3.0, with improved reporting of compiler

 errors and run-time exceptions, including detailed source positions.

 * Structure Name_Space (formerly NameSpace) now manages uniquely

 identified entries, with some additional information such as source

 position, logical grouping etc.

 * Theory and context data is now introduced by the simplified and

 modernized functors Theory_Data, Proof_Data, Generic_Data.  Data needs

 to be pure, but the old TheoryDataFun for mutable data (with explicit

 copy operation) is still available for some time.

 * Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)

 provides a high-level programming interface to synchronized state

 variables with atomic update.  This works via pure function

 application within a critical section -- its runtime should be as

 short as possible; beware of deadlocks if critical code is nested,

 either directly or indirectly via other synchronized variables!

 * Structure Unsynchronized (cf. src/Pure/ML-Systems/unsynchronized.ML)

 wraps raw ML references, explicitly indicating their non-thread-safe

 behaviour.  The Isar toplevel keeps this structure open, to

 accommodate Proof General as well as quick and dirty interactive

 experiments with references.

 * PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for

 parallel tactical reasoning.

 * Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS

 are similar to SUBPROOF, but are slightly more flexible: only the

 specified parts of the subgoal are imported into the context, and the

 body tactic may introduce new subgoals and schematic variables.

 * Old tactical METAHYPS, which does not observe the proof context, has

 been renamed to Old_Goals.METAHYPS and awaits deletion.  Use SUBPROOF

 or Subgoal.FOCUS etc.

 * Renamed functor TableFun to Table, and GraphFun to Graph.  (Since

 functors have their own ML name space there is no point to mark them

 separately.)  Minor INCOMPATIBILITY.

 * Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.

 * Renamed several structures FooBar to Foo_Bar.  Occasional,

 INCOMPATIBILITY.

 * Operations of structure Skip_Proof no longer require quick_and_dirty

 mode, which avoids critical setmp.

 * Eliminated old Attrib.add_attributes, Method.add_methods and related

 combinators for "args".  INCOMPATIBILITY, need to use simplified

 Attrib/Method.setup introduced in Isabelle2009.

 * Proper context for simpset_of, claset_of, clasimpset_of.  May fall

 back on global_simpset_of, global_claset_of, global_clasimpset_of as

 last resort.  INCOMPATIBILITY.

 * Display.pretty_thm now requires a proper context (cf. former

 ProofContext.pretty_thm).  May fall back on Display.pretty_thm_global

 or even Display.pretty_thm_without_context as last resort.

 INCOMPATIBILITY.

 * Discontinued Display.pretty_ctyp/cterm etc.  INCOMPATIBILITY, use

 Syntax.pretty_typ/term directly, preferably with proper context

 instead of global theory.

 *** System ***

 * Further fine tuning of parallel proof checking, scales up to 8 cores

 (max. speedup factor 5.0).  See also Goal.parallel_proofs in ML and

 usedir option -q.

 * Support for additional "Isabelle components" via etc/components, see

 also the system manual.

 * The isabelle makeall tool now operates on all components with

 IsaMakefile, not just hardwired "logics".

 * Removed "compress" option from isabelle-process and isabelle usedir;

 this is always enabled.

 * Discontinued support for Poly/ML 4.x versions.

 * Isabelle tool "wwwfind" provides web interface for 'find_theorems'

 on a given logic image.  This requires the lighttpd webserver and is

 currently supported on Linux only.

 New in Isabelle2009 (April 2009)

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

 *** General ***

 * Simplified main Isabelle executables, with less surprises on

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

   - The main Isabelle tool wrapper is now called "isabelle" instead of

     "isatool."

   - The former "isabelle" alias for "isabelle-process" has been

     removed (should rarely occur to regular users).

   - The former "isabelle-interface" and its alias "Isabelle" have been

     removed (interfaces are now regular Isabelle tools).

 Within scripts and make files, the Isabelle environment variables

 ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE,

 respectively.  (The latter are still available as legacy feature.)

 The old isabelle-interface wrapper could react in confusing ways if

 the interface was uninstalled or changed otherwise.  Individual

 interface tool configuration is now more explicit, see also the

 Isabelle system manual.  In particular, Proof General is now available

 via "isabelle emacs".

 INCOMPATIBILITY, need to adapt derivative scripts.  Users may need to

 purge installed copies of Isabelle executables and re-run "isabelle

 install -p ...", or use symlinks.

 * The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the

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

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

 INCOMPATIBILITY, need to move existing ~/isabelle/etc,

 ~/isabelle/heaps, ~/isabelle/browser_info to the new place.  Special

 care is required when using older releases of Isabelle.  Note that

 ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any

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

 * Proofs of fully specified statements are run in parallel on

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

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

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

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

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

 as hyperlinks are now available uniformly.

 *** Pure ***

 * Complete re-implementation of locales.  INCOMPATIBILITY in several

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

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

 - In locale expressions, instantiation replaces renaming.  Parameters

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

 parameter inheritance, in locale declarations, parameters that are not

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

 with their syntax at the beginning of the for clause.

 - Syntax from abbreviations and definitions in locales is available in

 locale expressions and context elements.  The latter is particularly

 useful in locale declarations.

 - More flexible mechanisms to qualify names generated by locale

 expressions.  Qualifiers (prefixes) may be specified in locale

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

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

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

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

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

 implicit qualifiers derived from the parameter names of a locale are

 no longer generated.

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

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

 brackets) is no longer available.  Use locale expressions.

 - When converting proof scripts, mandatory qualifiers in

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

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

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

 in locale expressions range over a single locale instance only.

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

 In existing theorem specifications replace the includes element by the

 respective context elements of the included locale, omitting those

 that are already present in the theorem specification.  Multiple

 assume elements of a locale should be replaced by a single one

 involving the locale predicate.  In the proof body, declarations (most

 notably theorems) may be regained by interpreting the respective

 locales in the proof context as required (command "interpret").

 If using "includes" in replacement of a target solely because the

 parameter types in the theorem are not as general as in the target,

 consider declaring a new locale with additional type constraints on

 the parameters (context element "constrains").

 - Discontinued "locale (open)".  INCOMPATIBILITY.

 - Locale interpretation commands no longer attempt to simplify goal.

 INCOMPATIBILITY: in rare situations the generated goal differs.  Use

 methods intro_locales and unfold_locales to clarify.

 - Locale interpretation commands no longer accept interpretation

 attributes.  INCOMPATIBILITY.

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

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

 in HOL, write

     class foo = ...

 instead of

     class foo = type + ...

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

 parameter prefix any longer.  INCOMPATIBILITY.

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

 INCOMPATIBILITY, use proper 'instantiation' target instead.

 * 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.

 * Slightly more coherent Pure syntax, with updated documentation in

 isar-ref manual.  Removed locales meta_term_syntax and

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

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

 directly in regular applications.

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

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

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

 interface with 'setup' command instead.

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

 theory context.

 * The 'axiomatization' command now only works within a global theory

 context.  INCOMPATIBILITY.

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

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

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

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

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

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

   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 generators.  Thus [code

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

 * Command 'find_consts' searches for constants based on type and name

 patterns, e.g.

     find_consts "_ => bool"

 By default, matching is against subtypes, but it may be restricted to

 the whole type.  Searching by name is possible.  Multiple queries are

 conjunctive and queries may be negated by prefixing them with a

 hyphen:

     find_consts strict: "_ => bool" name: "Int" -"int => int"

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

 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.

 *** Document preparation ***

 * Antiquotation @{lemma} now imitates a regular terminal proof,

 demanding keyword 'by' and supporting the full method expression

 syntax just like the Isar command 'by'.

 *** HOL ***

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

 points Main and Complex_Main remain as before.

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

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

 experimentation and tool development.  Note that user applications

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

 Main, as before.

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

 experimentation due to shorter build times.

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

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

 remains valid, but theories formerly using Complex_Main should now use

 new entry point Hypercomplex.

 * 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.

 * 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:

     op Int ~>   Set.Int

     op Un ~>    Set.Un

     INTER ~>    Set.INTER

     UNION ~>    Set.UNION

     Inter ~>    Set.Inter

     Union ~>    Set.Union

     {} ~>       Set.empty

     UNIV ~>     Set.UNIV

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

 theory Set.

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

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

 * Leibnitz's Series for Pi and the arcus tangens and logarithm series.

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

 Dense_Linear_Order) are now in directory HOL/Decision_Procs.

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

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

 interval arithmetic.  In the formulas are also the transcendental

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

 allowed. For examples see

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

 * Theory "Reflection" now resides in HOL/Library.

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

 INCOMPATIBILITY.

 * Made source layout more coherent with logical distribution

 structure:

     src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy

     src/HOL/Library/Code_Message.thy ~> src/HOL/

     src/HOL/Library/GCD.thy ~> src/HOL/

     src/HOL/Library/Order_Relation.thy ~> src/HOL/

     src/HOL/Library/Parity.thy ~> src/HOL/

     src/HOL/Library/Univ_Poly.thy ~> src/HOL/

     src/HOL/Real/ContNotDenum.thy ~> src/HOL/Library/

     src/HOL/Real/Lubs.thy ~> src/HOL/

     src/HOL/Real/PReal.thy ~> src/HOL/

     src/HOL/Real/Rational.thy ~> src/HOL/

     src/HOL/Real/RComplete.thy ~> src/HOL/

     src/HOL/Real/RealDef.thy ~> src/HOL/

     src/HOL/Real/RealPow.thy ~> src/HOL/

     src/HOL/Real/Real.thy ~> src/HOL/

     src/HOL/Complex/Complex_Main.thy ~> src/HOL/

     src/HOL/Complex/Complex.thy ~> src/HOL/

     src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/Library/

     src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~> src/HOL/Library/

     src/HOL/Hyperreal/Deriv.thy ~> src/HOL/

     src/HOL/Hyperreal/Fact.thy ~> src/HOL/

     src/HOL/Hyperreal/Integration.thy ~> src/HOL/

     src/HOL/Hyperreal/Lim.thy ~> src/HOL/

     src/HOL/Hyperreal/Ln.thy ~> src/HOL/

     src/HOL/Hyperreal/Log.thy ~> src/HOL/

     src/HOL/Hyperreal/MacLaurin.thy ~> src/HOL/

     src/HOL/Hyperreal/NthRoot.thy ~> src/HOL/

     src/HOL/Hyperreal/Series.thy ~> src/HOL/

     src/HOL/Hyperreal/SEQ.thy ~> src/HOL/

     src/HOL/Hyperreal/Taylor.thy ~> src/HOL/

     src/HOL/Hyperreal/Transcendental.thy ~> src/HOL/

     src/HOL/Real/Float ~> src/HOL/Library/

     src/HOL/Real/HahnBanach ~> src/HOL/HahnBanach

     src/HOL/Real/RealVector.thy ~> src/HOL/

     src/HOL/arith_data.ML ~> src/HOL/Tools

     src/HOL/hologic.ML ~> src/HOL/Tools

     src/HOL/simpdata.ML ~> src/HOL/Tools

     src/HOL/int_arith1.ML ~> src/HOL/Tools/int_arith.ML

     src/HOL/int_factor_simprocs.ML ~> src/HOL/Tools

     src/HOL/nat_simprocs.ML ~> src/HOL/Tools

     src/HOL/Real/float_arith.ML ~> src/HOL/Tools

     src/HOL/Real/float_syntax.ML ~> src/HOL/Tools

     src/HOL/Real/rat_arith.ML ~> src/HOL/Tools

     src/HOL/Real/real_arith.ML ~> src/HOL/Tools

     src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL

     src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL

     src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL

     src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL

     src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL

     src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL

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

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

 possible), avoiding strange error messages.

 * Method "sizechange" automates termination proofs using (a

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

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

 * Simplifier: simproc for let expressions now unfolds if bound

 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"

 Global usage is discouraged because of possible performance impact.

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

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

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

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

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

 INCOMPATIBILITY.

 * Theory 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.

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

 INCOMPATIBILITY: Instantiation proofs for order, linorder

 etc. slightly changed.  Some theorems named order_class.* now named

 preorder_class.*.

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

 "diag" to "Id_on".

 * Theory Finite_Set: added a new fold combinator of type

   ('a => 'b => 'b) => 'b => 'a set => 'b

 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.

 * Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps"

 and "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 at some point.

 * 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:

 rat_power_0    -> power_0

 rat_power_Suc  -> power_Suc

 realpow_0      -> power_0

 realpow_Suc    -> power_Suc

 complexpow_0   -> power_0

 complexpow_Suc -> power_Suc

 power_poly_0   -> power_0

 power_poly_Suc -> power_Suc

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

 moved to separate class dvd in Ring_and_Field; a couple of lemmas on

 dvd has been generalized to class comm_semiring_1.  Likewise a bunch

 of lemmas from Divides has been generalized from nat to class

 semiring_div.  INCOMPATIBILITY.  This involves the following theorem

 renames resulting from duplicate elimination:

     dvd_def_mod ~>          dvd_eq_mod_eq_0

     zero_dvd_iff ~>         dvd_0_left_iff

     dvd_0 ~>                dvd_0_right

     DIVISION_BY_ZERO_DIV ~> div_by_0

     DIVISION_BY_ZERO_MOD ~> mod_by_0

     mult_div ~>             div_mult_self2_is_id

     mult_mod ~>             mod_mult_self2_is_0

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

 generalizations (from Divides and Ring_and_Field).  INCOMPATIBILITY,

 rename old lemmas as follows:

 dvd_diff               -> nat_dvd_diff

 dvd_zminus_iff         -> dvd_minus_iff

 mod_add1_eq            -> mod_add_eq

 mod_mult1_eq           -> mod_mult_right_eq

 mod_mult1_eq'          -> mod_mult_left_eq

 mod_mult_distrib_mod   -> mod_mult_eq

 nat_mod_add_left_eq    -> mod_add_left_eq

 nat_mod_add_right_eq   -> mod_add_right_eq

 nat_mod_div_trivial    -> mod_div_trivial

 nat_mod_mod_trivial    -> mod_mod_trivial

 zdiv_zadd_self1        -> div_add_self1

 zdiv_zadd_self2        -> div_add_self2

 zdiv_zmult_self1       -> div_mult_self2_is_id

 zdiv_zmult_self2       -> div_mult_self1_is_id

 zdvd_triv_left         -> dvd_triv_left

 zdvd_triv_right        -> dvd_triv_right

 zdvd_zmult_cancel_disj -> dvd_mult_cancel_left

 zmod_eq0_zdvd_iff      -> dvd_eq_mod_eq_0[symmetric]

 zmod_zadd_left_eq      -> mod_add_left_eq

 zmod_zadd_right_eq     -> mod_add_right_eq

 zmod_zadd_self1        -> mod_add_self1

 zmod_zadd_self2        -> mod_add_self2

 zmod_zadd1_eq          -> mod_add_eq

 zmod_zdiff1_eq         -> mod_diff_eq

 zmod_zdvd_zmod         -> mod_mod_cancel

 zmod_zmod_cancel       -> mod_mod_cancel

 zmod_zmult_self1       -> mod_mult_self2_is_0

 zmod_zmult_self2       -> mod_mult_self1_is_0

 zmod_1                 -> mod_by_1

 zdiv_1                 -> div_by_1

 zdvd_abs1              -> abs_dvd_iff

 zdvd_abs2              -> dvd_abs_iff

 zdvd_refl              -> dvd_refl

 zdvd_trans             -> dvd_trans

 zdvd_zadd              -> dvd_add

 zdvd_zdiff             -> dvd_diff

 zdvd_zminus_iff        -> dvd_minus_iff

 zdvd_zminus2_iff       -> minus_dvd_iff

 zdvd_zmultD            -> dvd_mult_right

 zdvd_zmultD2           -> dvd_mult_left

 zdvd_zmult_mono        -> mult_dvd_mono

 zdvd_0_right           -> dvd_0_right

 zdvd_0_left            -> dvd_0_left_iff

 zdvd_1_left            -> one_dvd

 zminus_dvd_iff         -> minus_dvd_iff

 * 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,

 zlcm (for int); carried together from various gcd/lcm developements in

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

 ilcm; corresponding theorems renamed accordingly.  INCOMPATIBILITY,

 may recover tupled syntax as follows:

     hide (open) const gcd

     abbreviation gcd where

       "gcd == (%(a, b). GCD.gcd a b)"

     notation (output)

       GCD.gcd ("gcd '(_, _')")

 The same works for lcm, zgcd, zlcm.

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

 instantiations for algebraic structures.  Removed some duplicate

 theorems.  Changes in simp rules.  INCOMPATIBILITY.

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

 corresponding code in background and inserts name of the corresponding

 resulting ML value/function/datatype constructor binding in place.

 All occurrences of @{code} with a single ML block are generated

 simultaneously.  Provides a generic and safe interface for

 instrumentalizing code generation.  See

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

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

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

 cannot refer to constants for which user-defined serializations are

 set.  Refer to the corresponding ML counterpart directly in that

 cases.

 * Command 'rep_datatype': instead of theorem names the command now

 takes a list of terms denoting the constructors of the type to be

 represented as datatype.  The characteristic theorems have to be

 proven.  INCOMPATIBILITY.  Also observe that the following theorems

 have disappeared in favour of existing ones:

     unit_induct                 ~> unit.induct

     prod_induct                 ~> prod.induct

     sum_induct                  ~> sum.induct

     Suc_Suc_eq                  ~> nat.inject

     Suc_not_Zero Zero_not_Suc   ~> nat.distinct

 *** HOL-Algebra ***

 * New locales for orders and lattices where the equivalence relation

 is not restricted to equality.  INCOMPATIBILITY: all order and lattice

 locales use a record structure with field eq for the equivalence.

 * New theory of factorial domains.

 * Units_l_inv and Units_r_inv are now simp rules by default.

 INCOMPATIBILITY.  Simplifier proof that require deletion of l_inv

 and/or r_inv will now also require deletion of these lemmas.

 * Renamed the following theorems, INCOMPATIBILITY:

 UpperD ~> Upper_memD

 LowerD ~> Lower_memD

 least_carrier ~> least_closed

 greatest_carrier ~> greatest_closed

 greatest_Lower_above ~> greatest_Lower_below

 one_zero ~> carrier_one_zero

 one_not_zero ~> carrier_one_not_zero  (collision with assumption)

 *** HOL-Nominal ***

 * Nominal datatypes can now contain type-variables.

 * Commands 'nominal_inductive' and 'equivariance' work with local

 theory targets.

 * Nominal primrec can now works with local theory targets and its

 specification syntax now conforms to the general format as seen in

 'inductive' etc.

 * Method "perm_simp" honours the standard simplifier attributes

 (no_asm), (no_asm_use) etc.

 * The new predicate #* is defined like freshness, except that on the

 left hand side can be a set or list of atoms.

 * Experimental command 'nominal_inductive2' derives strong induction

 principles for inductive definitions.  In contrast to

 'nominal_inductive', which can only deal with a fixed number of

 binders, it can deal with arbitrary expressions standing for sets of

 atoms to be avoided.  The only inductive definition we have at the

 moment that needs this generalisation is the typing rule for Lets in

 the algorithm W:

  Gamma |- t1 : T1   (x,close Gamma T1)::Gamma |- t2 : T2   x#Gamma

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

          Gamma |- Let x be t1 in t2 : T2

 In this rule one wants to avoid all the binders that are introduced by

 "close Gamma T1".  We are looking for other examples where this

 feature might be useful.  Please let us know.

 *** HOLCF ***

 * Reimplemented the simplification procedure for proving continuity

 subgoals.  The new simproc is extensible; users can declare additional

 continuity introduction rules with the attribute [cont2cont].

 * The continuity simproc now uses a different introduction rule for

 solving continuity subgoals on terms with lambda abstractions.  In

 some rare cases the new simproc may fail to solve subgoals that the

 old one could solve, and "simp add: cont2cont_LAM" may be necessary.

 Potential INCOMPATIBILITY.

 * Command 'fixrec': specification syntax now conforms to the general

 format as seen in 'inductive' etc.  See src/HOLCF/ex/Fixrec_ex.thy for

 examples.  INCOMPATIBILITY.

 *** ZF ***

 * Proof of Zorn's Lemma for partial orders.

 *** ML ***

 * Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for

 Poly/ML 5.2.1 or later.  Important note: the TimeLimit facility

 depends on multithreading, so timouts will not work before Poly/ML

 5.2.1!

 * High-level support for concurrent ML programming, see

 src/Pure/Cuncurrent.  The data-oriented model of "future values" is

 particularly convenient to organize independent functional

 computations.  The concept of "synchronized variables" provides a

 higher-order interface for components with shared state, avoiding the

 delicate details of mutexes and condition variables.  (Requires

 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.)

 * Simplified ML attribute and method setup, cf. functions Attrib.setup

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

 'method_setup'.  INCOMPATIBILITY for 'method_setup', need to simplify

 existing code accordingly, or use plain 'setup' together with old

 Method.add_method.

 * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm

 to 'a -> thm, while results are always tagged with an authentic oracle

 name.  The Isar command 'oracle' is now polymorphic, no argument type

 is specified.  INCOMPATIBILITY, need to simplify existing oracle code

 accordingly.  Note that extra performance may be gained by producing

 the cterm carefully, avoiding slow Thm.cterm_of.

 * Simplified interface for defining document antiquotations via

 ThyOutput.antiquotation, ThyOutput.output, and optionally

 ThyOutput.maybe_pretty_source.  INCOMPATIBILITY, need to simplify user

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

 examples.

 * More systematic treatment of long names, abstract name bindings, and

 name space operations.  Basic operations on qualified names have been

 move from structure NameSpace to Long_Name, e.g. Long_Name.base_name,

 Long_Name.append.  Old type bstring has been mostly replaced by

 abstract type binding (see structure Binding), which supports precise

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

 tracking of source positions.  INCOMPATIBILITY, need to wrap old

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

 bindings everywhere.  See further src/Pure/General/long_name.ML,

 src/Pure/General/binding.ML and src/Pure/General/name_space.ML

 * Result facts (from PureThy.note_thms, ProofContext.note_thms,

 LocalTheory.note etc.) now refer to the *full* internal name, not the

 bstring as before.  INCOMPATIBILITY, not detected by ML type-checking!

 * Disposed old type and term read functions (Sign.read_def_typ,

 Sign.read_typ, Sign.read_def_terms, Sign.read_term,

 Thm.read_def_cterms, Thm.read_cterm etc.).  INCOMPATIBILITY, should

 use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global,

 Syntax.read_term_global etc.; see also OldGoals.read_term as last

 resort for legacy applications.

 * Disposed old declarations, tactics, tactic combinators that refer to

 the simpset or claset of an implicit theory (such as Addsimps,

 Simp_tac, SIMPSET).  INCOMPATIBILITY, should use @{simpset} etc. in

 embedded ML text, or local_simpset_of with a proper context passed as

 explicit runtime argument.

 * 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

 \<lbrace> ... \<rbrace>; additional antiquotation forms:

   @{binding name}                         - basic name binding

   @{let ?pat = term}                      - term abbreviation (HO matching)

   @{note name = fact}                     - fact abbreviation

   @{thm fact}                             - singleton fact (with attributes)

   @{thms fact}                            - general fact (with attributes)

   @{lemma prop by method}                 - singleton goal

   @{lemma prop by meth1 meth2}            - singleton goal

   @{lemma prop1 ... propN by method}      - general goal

   @{lemma prop1 ... propN by meth1 meth2} - general goal

   @{lemma (open) ...}                     - open derivation

 *** System ***

 * The Isabelle "emacs" tool provides a specific interface to invoke

 Proof General / Emacs, with more explicit failure if that is not

 installed (the old isabelle-interface script silently falls back on

 isabelle-process).  The PROOFGENERAL_HOME setting determines the

 installation location of the Proof General distribution.

 * Isabelle/lib/classes/Pure.jar provides basic support to integrate

 the Isabelle process into a JVM/Scala application.  See

 Isabelle/lib/jedit/plugin for a minimal example.  (The obsolete Java

 process wrapper has been discontinued.)

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

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

 emitted, if proper markup print mode is enabled.  This allows

 user-interface components to provide detailed feedback on internal

 prover operations.

 New in Isabelle2008 (June 2008)

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

 *** General ***

 * The Isabelle/Isar Reference Manual (isar-ref) has been reorganized

 and updated, with formally checked references as hyperlinks.

 * Theory loader: use_thy (and similar operations) no longer set the

 implicit ML context, which was occasionally hard to predict and in

 conflict with concurrency.  INCOMPATIBILITY, use ML within Isar which

 provides a proper context already.

 * Theory loader: old-style ML proof scripts being *attached* to a thy

 file are no longer supported.  INCOMPATIBILITY, regular 'uses' and

 'use' within a theory file will do the job.

 * Name space merge now observes canonical order, i.e. the second space

 is inserted into the first one, while existing entries in the first

 space take precedence.  INCOMPATIBILITY in rare situations, may try to

 swap theory imports.

 * Syntax: symbol \<chi> is now considered a letter.  Potential

 INCOMPATIBILITY in identifier syntax etc.

 * Outer syntax: string tokens no longer admit escaped white space,

 which was an accidental (undocumented) feature.  INCOMPATIBILITY, use

 white space without escapes.

 * Outer syntax: string tokens may contain arbitrary character codes

 specified via 3 decimal digits (as in SML).  E.g. "foo\095bar" for

 "foo_bar".

 *** Pure ***

 * Context-dependent token translations.  Default setup reverts locally

 fixed variables, and adds hilite markup for undeclared frees.

 * Unused theorems can be found using the new command 'unused_thms'.

 There are three ways of invoking it:

 (1) unused_thms

      Only finds unused theorems in the current theory.

 (2) unused_thms thy_1 ... thy_n -

      Finds unused theorems in the current theory and all of its ancestors,

      excluding the theories thy_1 ... thy_n and all of their ancestors.

 (3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m

      Finds unused theorems in the theories thy'_1 ... thy'_m and all of

      their ancestors, excluding the theories thy_1 ... thy_n and all of

      their ancestors.

 In order to increase the readability of the list produced by

 unused_thms, theorems that have been created by a particular instance

 of a theory command such as 'inductive' or 'function' are considered

 to belong to the same "group", meaning that if at least one theorem in

 this group is used, the other theorems in the same group are no longer

 reported as unused.  Moreover, if all theorems in the group are

 unused, only one theorem in the group is displayed.

 Note that proof objects have to be switched on in order for

 unused_thms to work properly (i.e. !proofs must be >= 1, which is

 usually the case when using Proof General with the default settings).

 * Authentic naming of facts disallows ad-hoc overwriting of previous

 theorems within the same name space.  INCOMPATIBILITY, need to remove

 duplicate fact bindings, or even accidental fact duplications.  Note

 that tools may maintain dynamically scoped facts systematically, using

 PureThy.add_thms_dynamic.

 * Command 'hide' now allows to hide from "fact" name space as well.

 * Eliminated destructive theorem database, simpset, claset, and

 clasimpset.  Potential INCOMPATIBILITY, really need to observe linear

 update of theories within ML code.

 * Eliminated theory ProtoPure and CPure, leaving just one Pure theory.

 INCOMPATIBILITY, object-logics depending on former Pure require

 additional setup PureThy.old_appl_syntax_setup; object-logics

 depending on former CPure need to refer to Pure.

 * Commands 'use' and 'ML' are now purely functional, operating on

 theory/local_theory.  Removed former 'ML_setup' (on theory), use 'ML'

 instead.  Added 'ML_val' as mere diagnostic replacement for 'ML'.

 INCOMPATIBILITY.

 * Command 'setup': discontinued implicit version with ML reference.

 * Instantiation target allows for simultaneous specification of class

 instance operations together with an instantiation proof.

 Type-checking phase allows to refer to class operations uniformly.

 See src/HOL/Complex/Complex.thy for an Isar example and

 src/HOL/Library/Eval.thy for an ML example.

 * Indexing of literal facts: be more serious about including only

 facts from the visible specification/proof context, but not the

 background context (locale etc.).  Affects `prop` notation and method

 "fact".  INCOMPATIBILITY: need to name facts explicitly in rare

 situations.

 * Method "cases", "induct", "coinduct": removed obsolete/undocumented

 "(open)" option, which used to expose internal bound variables to the

 proof text.

 * Isar statements: removed obsolete case "rule_context".

 INCOMPATIBILITY, better use explicit fixes/assumes.

 * Locale proofs: default proof step now includes 'unfold_locales';

 hence 'proof' without argument may be used to unfold locale

 predicates.

 *** Document preparation ***

 * Simplified pdfsetup.sty: color/hyperref is used unconditionally for

 both pdf and dvi (hyperlinks usually work in xdvi as well); removed

 obsolete thumbpdf setup (contemporary PDF viewers do this on the

 spot); renamed link color from "darkblue" to "linkcolor" (default

 value unchanged, can be redefined via \definecolor); no longer sets

 "a4paper" option (unnecessary or even intrusive).

 * Antiquotation @{lemma A method} proves proposition A by the given

 method (either a method name or a method name plus (optional) method

 arguments in parentheses) and prints A just like @{prop A}.

 *** HOL ***

 * New primrec package.  Specification syntax conforms in style to

 definition/function/....  No separate induction rule is provided.  The

 "primrec" command distinguishes old-style and new-style specifications

 by syntax.  The former primrec package is now named OldPrimrecPackage.

 When adjusting theories, beware: constants stemming from new-style

 primrec specifications have authentic syntax.

 * Metis prover is now an order of magnitude faster, and also works

 with multithreading.

 * Metis: the maximum number of clauses that can be produced from a

 theorem is now given by the attribute max_clauses.  Theorems that

 exceed this number are ignored, with a warning printed.

 * Sledgehammer no longer produces structured proofs by default. To

 enable, declare [[sledgehammer_full = true]].  Attributes

 reconstruction_modulus, reconstruction_sorts renamed

 sledgehammer_modulus, sledgehammer_sorts.  INCOMPATIBILITY.

 * Method "induct_scheme" derives user-specified induction rules

 from well-founded induction and completeness of patterns. This factors

 out some operations that are done internally by the function package

 and makes them available separately.  See

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

 * More flexible generation of measure functions for termination

 proofs: Measure functions can be declared by proving a rule of the

 form "is_measure f" and giving it the [measure_function] attribute.

 The "is_measure" predicate is logically meaningless (always true), and

 just guides the heuristic.  To find suitable measure functions, the

 termination prover sets up the goal "is_measure ?f" of the appropriate

 type and generates all solutions by prolog-style backwards proof using

 the declared rules.

 This setup also deals with rules like 

   "is_measure f ==> is_measure (list_size f)"

 which accommodates nested datatypes that recurse through lists.

 Similar rules are predeclared for products and option types.

 * Turned the type of sets "'a set" into an abbreviation for "'a => bool"

   INCOMPATIBILITIES:

   - Definitions of overloaded constants on sets have to be replaced by

     definitions on => and bool.

   - Some definitions of overloaded operators on sets can now be proved

     using the definitions of the operators on => and bool.  Therefore,

     the following theorems have been renamed:

       subset_def   -> subset_eq

       psubset_def  -> psubset_eq

       set_diff_def -> set_diff_eq

       Compl_def    -> Compl_eq

       Sup_set_def  -> Sup_set_eq

       Inf_set_def  -> Inf_set_eq

       sup_set_def  -> sup_set_eq

       inf_set_def  -> inf_set_eq

   - Due to the incompleteness of the HO unification algorithm, some

     rules such as subst may require manual instantiation, if some of

     the unknowns in the rule is a set.

   - Higher order unification and forward proofs:

     The proof pattern

       have "P (S::'a set)" <...>

       then have "EX S. P S" ..

     no longer works (due to the incompleteness of the HO unification

     algorithm) and must be replaced by the pattern

       have "EX S. P S"

       proof

         show "P S" <...>

       qed

   - Calculational reasoning with subst (or similar rules):

     The proof pattern

       have "P (S::'a set)" <...>

       also have "S = T" <...>

       finally have "P T" .

     no longer works (for similar reasons as the previous example) and

     must be replaced by something like

       have "P (S::'a set)" <...>

       moreover have "S = T" <...>

       ultimately have "P T" by simp

   - Tactics or packages written in ML code:

     Code performing pattern matching on types via

       Type ("set", [T]) => ...