Isabelle NEWS -- history user-relevant changes

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

 New in this Isabelle version

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

 *** General ***

 * Theory loader: source files are identified by content via SHA1

 digests.  Discontinued former path/modtime identification and optional

 ISABELLE_FILE_IDENT plugin scripts.

 * Parallelization of nested Isar proofs is subject to

 Goal.parallel_proofs_threshold (default 100).  See also isabelle

 usedir option -Q.

 * Discontinued support for Poly/ML 5.2, which was the last version

 without proper multithreading and TimeLimit implementation.

 * Discontinued old lib/scripts/polyml-platform, which has been

 obsolete since Isabelle2009-2.

 * Theory loader: source files are exclusively located via the master

 directory of each theory node (where the .thy file itself resides).

 The global load path (such as src/HOL/Library) is has been

 discontinued.  INCOMPATIBILITY.

 * Various optional external tools are referenced more robustly and

 uniformly by explicit Isabelle settings as follows:

   ISABELLE_CSDP   (formerly CSDP_EXE)

   ISABELLE_GHC    (formerly EXEC_GHC or GHC_PATH)

   ISABELLE_OCAML  (formerly EXEC_OCAML)

   ISABELLE_SWIPL  (formerly EXEC_SWIPL)

   ISABELLE_YAP    (formerly EXEC_YAP)

 Note that automated detection from the file-system or search path has

 been discontinued.  INCOMPATIBILITY.

 *** HOL ***

 * Nitpick:

   - Added "need" and "total_consts" options.

   - Reintroduced "show_skolems" option by popular demand.

   - Renamed attribute: nitpick_def ~> nitpick_unfold.

     INCOMPATIBILITY.

 * Sledgehammer:

   - sledgehammer available_provers ~> sledgehammer supported_provers

     INCOMPATIBILITY.

 * Function package: discontinued option "tailrec".

 INCOMPATIBILITY. Use partial_function instead.

 *** Document preparation ***

 * New term style "isub" as ad-hoc conversion of variables x1, y23 into

 subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.

 *** ML ***

 * Path.print is the official way to show file-system paths to users

 (including quotes etc.).

 New in Isabelle2011 (January 2011)

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

 *** General ***

 * Experimental Prover IDE based on Isabelle/Scala and jEdit (see

 src/Tools/jEdit).  This also serves as IDE for Isabelle/ML, with

 useful tooltips and hyperlinks produced from its static analysis.  The

 bundled component provides an executable Isabelle tool that can be run

 like this:

   Isabelle2011/bin/isabelle jedit

 * Significantly improved Isabelle/Isar implementation manual.

 * System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER

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

 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.

 * Source files are always encoded as UTF-8, instead of old-fashioned

 ISO-Latin-1.  INCOMPATIBILITY.  Isabelle LaTeX documents might require

 the following package declarations:

   \usepackage[utf8]{inputenc}

   \usepackage{textcomp}

 * Explicit treatment of UTF-8 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 loader: source files are primarily located via the master

 directory of each theory node (where the .thy file itself resides).

 The global load path is still partially available as legacy feature.

 Minor INCOMPATIBILITY due to subtle change in file lookup: use

 explicit paths, relatively to the theory.

 * 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 or print modes.  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

   show_abbrevs                  show_abbrevs

   Syntax.ast_trace              syntax_ast_trace

   Syntax.ast_stat               syntax_ast_stat

   Syntax.ambiguity_level        syntax_ambiguity_level

   Goal_Display.goals_limit      goals_limit

   Goal_Display.show_main_goal   show_main_goal

   Method.rule_trace             rule_trace

   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 only be

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

 The option "show_abbrevs" supersedes the former print mode

 "no_abbrevs" with inverted meaning.

 * More systematic naming of some configuration options.

 INCOMPATIBILITY.

   trace_simp  ~>  simp_trace

   debug_simp  ~>  simp_debug

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

 front-ends need to accept "pgint" values in float notation.

 INCOMPATIBILITY.

 * The IsabelleText font now includes Cyrillic, Hebrew, Arabic from

 DejaVu Sans.

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

 *** Pure ***

 * Command 'type_synonym' (with single argument) replaces somewhat

 outdated 'types', which is still available as legacy feature for some

 time.

 * Command 'nonterminal' (with 'and' separated list of arguments)

 replaces somewhat outdated 'nonterminals'.  INCOMPATIBILITY.

 * Command 'notepad' replaces former 'example_proof' for

 experimentation in Isar without any result.  INCOMPATIBILITY.

 * Locale interpretation commands 'interpret' and 'sublocale' accept

 lists of equations to map definitions in a locale to appropriate

 entities in the context of the interpretation.  The 'interpretation'

 command already provided this functionality.

 * Diagnostic command 'print_dependencies' prints the locale instances

 that would be activated if the specified expression was interpreted in

 the current context.  Variant "print_dependencies!" assumes a context

 without interpretations.

 * 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 obsolete 'constdefs' command.  INCOMPATIBILITY, use

 'definition' instead.

 * The "prems" fact, which refers to the accidental collection of

 foundational premises in the context, is now explicitly marked as

 legacy feature and will be discontinued soon.  Consider using "assms"

 of the head statement or reference facts by explicit names.

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

 constructors.

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

 the local file system.

 *** HOL ***

 * Coercive subtyping: functions can be declared as coercions and type

 inference will add them as necessary upon input of a term.  Theory

 Complex_Main declares real :: nat => real and real :: int => real as

 coercions. A coercion function f is declared like this:

   declare [[coercion f]]

 To lift coercions through type constructors (e.g. from nat => real to

 nat list => real list), map functions can be declared, e.g.

   declare [[coercion_map map]]

 Currently coercion inference is activated only in theories including

 real numbers, i.e. descendants of Complex_Main.  This is controlled by

 the configuration option "coercion_enabled", e.g. it can be enabled in

 other theories like this:

   declare [[coercion_enabled]]

 * 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

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

 for examples.

 * Function package: f.psimps rules are no longer implicitly declared

 as [simp].  INCOMPATIBILITY.

 * Datatype package: theorems generated for executable equality (class

 "eq") carry proper names and are treated as default code equations.

 * Inductive package: now offers command 'inductive_simps' to

 automatically derive instantiated and simplified equations for

 inductive predicates, similar to 'inductive_cases'.

 * Command 'enriched_type' allows to register properties of the

 functorial structure of types.

 * Improved infrastructure for term evaluation using code generator

 techniques, in particular static evaluation conversions.

 * Code generator: Scala (2.8 or higher) has been added to the target

 languages.

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

 have been replaced by the more idiomatic "_" and "Theory._".

 INCOMPATIBILITY.

 * Code generator: export_code without explicit file declaration prints

 to standard output.  INCOMPATIBILITY.

 * Code generator: do not print function definitions for case

 combinators any longer.

 * Code generator: simplification with rules determined with

 src/Tools/Code/code_simp.ML and method "code_simp".

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

 * Records: logical foundation type for records does not carry a

 '_type' suffix any longer (obsolete due to authentic syntax).

 INCOMPATIBILITY.

 * Quickcheck now by default uses exhaustive testing instead of random

 testing.  Random testing can be invoked by "quickcheck [random]",

 exhaustive testing by "quickcheck [exhaustive]".

 * Quickcheck instantiates polymorphic types with small finite

 datatypes by default. This enables a simple execution mechanism to

 handle quantifiers and function equality over the finite datatypes.

 * Quickcheck random generator has been renamed from "code" to

 "random".  INCOMPATIBILITY.

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

 * Quickcheck in locales considers interpretations of that locale for

 counter example search.

 * Sledgehammer:

   - Added "smt" and "remote_smt" provers based on the "smt" proof

     method. See the Sledgehammer manual for details ("isabelle doc

     sledgehammer").

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

 * Nitpick:

   - Renamed options:

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

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

     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.

 * Proof methods "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]]

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

 manually as command 'solve_direct'.

 * The default SMT solver Z3 must be enabled explicitly (due to

 licensing issues) by setting the environment variable

 Z3_NON_COMMERCIAL in etc/settings of the component, for example.  For

 commercial applications, the SMT solver CVC3 is provided as fall-back;

 changing the SMT solver is done via the configuration option

 "smt_solver".

 * Remote SMT solvers need to be referred to by the "remote_" prefix,

 i.e. "remote_cvc3" and "remote_z3".

 * Added basic SMT support for datatypes, records, and typedefs using

 the oracle mode (no proofs).  Direct support of pairs has been dropped

 in exchange (pass theorems fst_conv snd_conv pair_collapse to the SMT

 support for a similar behavior).  Minor INCOMPATIBILITY.

 * Changed SMT configuration options:

   - Renamed:

     z3_proofs ~> smt_oracle (with inverted meaning)

     z3_trace_assms ~> smt_trace_used_facts

     INCOMPATIBILITY.

   - Added:

     smt_verbose

     smt_random_seed

     smt_datatypes

     smt_infer_triggers

     smt_monomorph_limit

     cvc3_options

     remote_cvc3_options

     remote_z3_options

     yices_options

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

 header.

 * Simplification procedure "list_to_set_comprehension" rewrites list

 comprehensions applied to List.set to set comprehensions.  Occasional

 INCOMPATIBILITY, may be deactivated like this:

   declare [[simproc del: list_to_set_comprehension]]

 * Removed old version of primrec package.  INCOMPATIBILITY.

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

 been the case with "split".  INCOMPATIBILITY.

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

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

 [split_format].  Potential INCOMPATIBILITY.

 * Predicate "sorted" now defined inductively, with nice induction

 rules.  INCOMPATIBILITY: former sorted.simps now named sorted_simps.

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

 contents for other uses.  INCOMPATIBILITY.

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

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

 tuning.  INCOMPATIBILITY.

 * Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.

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

 INCOMPATIBILITY.

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

 avoid confusion with finite sets.  INCOMPATIBILITY.

 * Abandoned locales equiv, congruent and congruent2 for equivalence

 relations.  INCOMPATIBILITY: use equivI rather than equiv_intro (same

 for congruent(2)).

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

 * More canonical naming convention for some fundamental definitions:

     bot_bool_eq ~> bot_bool_def

     top_bool_eq ~> top_bool_def

     inf_bool_eq ~> inf_bool_def

     sup_bool_eq ~> sup_bool_def

     bot_fun_eq  ~> bot_fun_def

     top_fun_eq  ~> top_fun_def

     inf_fun_eq  ~> inf_fun_def

     sup_fun_eq  ~> sup_fun_def

 INCOMPATIBILITY.

 * More stylized fact names:

   expand_fun_eq ~> fun_eq_iff

   expand_set_eq ~> set_eq_iff

   set_ext       ~> set_eqI

   nat_number    ~> eval_nat_numeral

 INCOMPATIBILITY.

 * Refactoring of code-generation specific operations in theory List:

   constants

     null ~> List.null

   facts

     mem_iff ~> member_def

     null_empty ~> null_def

 INCOMPATIBILITY.  Note that these were not supposed to be used

 regularly unless for striking reasons; their main purpose was code

 generation.

 Various operations from the Haskell prelude are used for generating

 Haskell code.

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

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

 bij_def and surj_def are unchanged.  INCOMPATIBILITY.

 * Abolished some non-alphabetic type names: "prod" and "sum" replace

 "*" and "+" respectively.  INCOMPATIBILITY.

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

 "Sum_Type.Plus" instead.

 * 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 "_ : set _"

 instead.  INCOMPATIBILITY.

 * Removed lemma "Option.is_none_none" which duplicates "is_none_def".

 INCOMPATIBILITY.

 * Former theory Library/Enum 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.

   enum    ~>  Enum.enum

   nlists  ~>  Enum.nlists

   product ~>  Enum.product

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

 Syntax in Library/State_Monad has been changed to avoid ambiguities.

 INCOMPATIBILITY.

 * Theory Library/SetsAndFunctions has been split into

 Library/Function_Algebras and Library/Set_Algebras; canonical names

 for instance definitions for functions; various improvements.

 INCOMPATIBILITY.

 * Theory Library/Multiset provides stable quicksort implementation of

 sort_key.

 * Theory Library/Multiset: renamed empty_idemp ~> empty_neutral.

 INCOMPATIBILITY.

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

 * Session Probability: introduced pextreal as positive extended real

 numbers.  Use pextreal as value for measures.  Introduce the

 Radon-Nikodym derivative, product spaces and Fubini's theorem for

 arbitrary sigma finite measures.  Introduces Lebesgue measure based on

 the integral in Multivariate Analysis.  INCOMPATIBILITY.

 * Session Imperative_HOL: revamped, corrected dozens of inadequacies.

 INCOMPATIBILITY.

 * Session SPARK (with image HOL-SPARK) provides commands to load and

 prove verification conditions generated by the SPARK Ada program

 verifier.  See also src/HOL/SPARK and src/HOL/SPARK/Examples.

 *** HOL-Algebra ***

 * Theorems for additive ring operations (locale abelian_monoid and

 descendants) are generated by interpretation from their multiplicative

 counterparts.  Names (in particular theorem names) have the mandatory

 qualifier 'add'.  Previous theorem names are redeclared for

 compatibility.

 * Structure "int_ring" is now an abbreviation (previously a

 definition).  This fits more natural with advanced interpretations.

 *** 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.  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 domain package (definitional mode) now supports unpointed

 predomain argument types, as long as they are marked 'lazy'. (Strict

 arguments must be in class "domain".) For example, the following

 domain definition now works:

   domain natlist = nil | cons (lazy "nat discr") (lazy "natlist")

 * Theory HOLCF/Library/HOL_Cpo provides cpo and predomain class

 instances for types from main HOL: bool, nat, int, char, 'a + 'b,

 'a option, and 'a list.  Additionally, it configures fixrec and the

 domain package to work with these types.  For example:

   fixrec isInl :: "('a + 'b) u -> tr"

     where "isInl$(up$(Inl x)) = TT" | "isInl$(up$(Inr y)) = FF"

   domain V = VFun (lazy "V -> V") | VCon (lazy "nat") (lazy "V list")

 * The "(permissive)" option of fixrec has been replaced with a

 per-equation "(unchecked)" option. See

 src/HOL/HOLCF/Tutorial/Fixrec_ex.thy for examples. INCOMPATIBILITY.

 * The "bifinite" class no longer fixes a constant "approx"; the class

 now just asserts that such a function exists.  INCOMPATIBILITY.

 * Former type "alg_defl" has been renamed to "defl".  HOLCF no longer

 defines an embedding of type 'a defl into udom by default; instances

 of "bifinite" and "domain" classes are available in

 src/HOL/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.

 * The function "cprod_map" has been renamed to "prod_map".

 INCOMPATIBILITY.

 * The monadic bind operator on each powerdomain has new binder syntax

 similar to sets, e.g. "\<Union>\<sharp>x\<in>xs. t" represents

 "upper_bind\<cdot>xs\<cdot>(\<Lambda> x. t)".

 * The infix syntax for binary union on each powerdomain has changed

 from e.g. "+\<sharp>" to "\<union>\<sharp>", for consistency with set

 syntax.  INCOMPATIBILITY.

 * The constant "UU" has been renamed to "bottom".  The syntax "UU" is

 still supported as an input translation.

 * 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

   lub_fun         ~> is_lub_fun

   thelub_fun      ~> lub_fun

   thelub_cfun     ~> lub_cfun

   thelub_Pair     ~> lub_Pair

   lub_cprod       ~> is_lub_prod

   thelub_cprod    ~> lub_prod

   minimal_cprod   ~> minimal_prod

   inst_cprod_pcpo ~> inst_prod_pcpo

   UU_I            ~> bottomI

   compact_UU      ~> compact_bottom

   deflation_UU    ~> deflation_bottom

   finite_deflation_UU ~> finite_deflation_bottom

 * 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 and ZF ***

 * All constant names are now qualified internally and use proper

 identifiers, e.g. "IFOL.eq" instead of "op =".  INCOMPATIBILITY.

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

 * Antiquotation @{theory A} refers to theory A from the ancestry of

 the current context, not any accidental theory loader state as before.

 Potential INCOMPATIBILITY, subtle change in semantics.

 * Syntax.pretty_priority (default 0) configures the required priority

 of pretty-printed output and thus affects insertion of parentheses.

 * Syntax.default_root (default "any") configures the inner syntax

 category (nonterminal symbol) for parsing of terms.

 * Former exception Library.UnequalLengths now coincides with

 ListPair.UnequalLengths.

 * Renamed structure MetaSimplifier to Raw_Simplifier.  Note that the

 main functionality is provided by structure Simplifier.

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

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

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

 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)

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