Isabelle NEWS -- history user-relevant changes

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

 New in Isabelle2009-2 (June 2010)

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

 *** General ***

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

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

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

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

 *** Pure ***

 * Predicates of locales introduces by classes carry a mandatory

 "class" prefix.  INCOMPATIBILITY.

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

 runtime environment; replaces immature code_datatype antiquotation.

 INCOMPATIBILITY.

 * Empty class specifications observe default sort.  INCOMPATIBILITY.

 * Old 'axclass' command has been discontinued.  Use 'class' instead.

 INCOMPATIBILITY.

 * Code generator: simple concept for abstract datatypes obeying

 invariants.

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

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

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

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

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

 order of type variables. Potential INCOMPATIBILITY for tools working

 with proof terms.

 *** HOL ***

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

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

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

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

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

     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.

 * HOLogic.strip_psplit: types are returned in syntactic order, similar

 to other strip and tuple operations.  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.

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

 clash with new theory Quotient in Main HOL.

 * 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

   - Improved precision of set constructs.

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

 * Moved the SMT binding into the HOL image.

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

 Proof scripts 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 ***

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

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

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

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

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

 as infinity (as in chop).  Subtle INCOMPATIBILITY.

 *** 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}"

 New in Isabelle2009-1 (December 2009)

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

 *** General ***

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

 one backslash should be used, even in ML sources.

 *** Pure ***

 * Locale interpretation propagates mixins along the locale hierarchy.

 The currently only available mixins are the equations used to map

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

 * Reactivated diagnostic command 'print_interps'.  Use "print_interps

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

 Interpretations in proofs are not shown.

 * Thoroughly revised locales tutorial.  New section on conditional

 interpretation.

 * On instantiation of classes, remaining undefined class parameters

 are formally declared.  INCOMPATIBILITY.

 *** Document preparation ***

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

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

 backward compatibility).  Styles can be also applied for

 antiquotations prop, term_type and typeof.

 *** HOL ***

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

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

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

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

 procedure based on external SMT solvers using the oracle mechanism;

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

 are provided to avoid calling the external solvers solely for

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

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

 * New commands to load and prove verification conditions generated by

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

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

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

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

 src/HOL/Nitpick_Examples.

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

 compiler and to enumerate values of inductive predicates.

 * A tabled implementation of the reflexive transitive closure.

 * New implementation of quickcheck uses generic code generator;

 default generators are provided for all suitable HOL types, records

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

 Library/SML_Quickcheck.

 * New testing tool Mirabelle for automated proof tools.  Applies

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

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

 "mirabelle" utility.

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

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

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

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

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

 inequalities between polynomials.  It makes use of external

 semidefinite programming solvers.  Method "sos" generates a

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

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

 src/HOL/Library/Sum_Of_Squares.

 * New method "linarith" invokes existing linear arithmetic decision

 procedure only.

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

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

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

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

 that fail later.

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

 information in order to avoid failures of proof reconstruction.

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

 the same method as the approximation method.

 * Method "approximate" now supports arithmetic expressions as

 boundaries of intervals and implements interval splitting and Taylor

 series expansion.

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

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

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

 reals.

 * New theory Probability, which contains a development of measure

 theory, eventually leading to Lebesgue integration and probability.

 * Extended Multivariate Analysis to include derivation and Brouwer's

 fixpoint theorem.

 * Reorganization of number theory, INCOMPATIBILITY:

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

     and GCD as well as in new session Number_Theory

   - some constants and facts now suffixed with _nat and _int

     accordingly

   - former session NumberTheory now named Old_Number_Theory, including

     theories Legacy_GCD and Primes (prefer Number_Theory if possible)

   - moved theory Pocklington from src/HOL/Library to

     src/HOL/Old_Number_Theory

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

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

 lattice.

 * Class semiring_div requires superclass no_zero_divisors and proof of

 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,

 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been

 generalized to class semiring_div, subsuming former theorems

 zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and

 zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.

 INCOMPATIBILITY.

 * Refinements to lattice classes and sets:

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

     intro/elim rules in class variant: more uniformity

   - lemma ge_sup_conv renamed to le_sup_iff, in accordance with

     le_inf_iff

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

     sup_aci)

   - renamed ACI to inf_sup_aci

   - new class "boolean_algebra"

   - class "complete_lattice" moved to separate theory

     "Complete_Lattice"; corresponding constants (and abbreviations)

     renamed and with authentic syntax:

     Set.Inf ~>    Complete_Lattice.Inf

     Set.Sup ~>    Complete_Lattice.Sup

     Set.INFI ~>   Complete_Lattice.INFI

     Set.SUPR ~>   Complete_Lattice.SUPR

     Set.Inter ~>  Complete_Lattice.Inter

     Set.Union ~>  Complete_Lattice.Union

     Set.INTER ~>  Complete_Lattice.INTER

     Set.UNION ~>  Complete_Lattice.UNION

   - authentic syntax for

     Set.Pow

     Set.image

   - mere abbreviations:

     Set.empty               (for bot)

     Set.UNIV                (for top)

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

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

     Complete_Lattice.Inter  (for Inf)

     Complete_Lattice.Union  (for Sup)

     Complete_Lattice.INTER  (for INFI)

     Complete_Lattice.UNION  (for SUPR)

   - object-logic definitions as far as appropriate

 INCOMPATIBILITY.  Care is required when theorems Int_subset_iff or

 Un_subset_iff are explicitly deleted as default simp rules; then also

 their lattice counterparts le_inf_iff and le_sup_iff have to be

 deleted to achieve the desired effect.

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

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

 etc.  INCOMPATIBILITY.

 * Rules sup_Int_eq and sup_Un_eq are no longer declared as

 pred_set_conv by default.  INCOMPATIBILITY.

 * Power operations on relations and functions are now one dedicated

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

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

 in class power.  INCOMPATIBILITY.

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

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

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

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

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

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

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

 INCOMPATIBILITY.

 * Most rules produced by inductive and datatype package have mandatory

 prefixes.  INCOMPATIBILITY.

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

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

 DERIV_intros assumes composition with an additional function and

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

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

 of most elementary terms.  Former Maclauren.DERIV_tac and

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

 INCOMPATIBILITY.

 * Code generator attributes follow the usual underscore convention:

     code_unfold     replaces    code unfold

     code_post       replaces    code post

     etc.

   INCOMPATIBILITY.

 * Renamed methods:

     sizechange -> size_change

     induct_scheme -> induction_schema

   INCOMPATIBILITY.

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

 INCOMPATIBILITY, use "undefined" directly.

 * Renamed theorems:

     Suc_eq_add_numeral_1 -> Suc_eq_plus1

     Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left

     Suc_plus1 -> Suc_eq_plus1

     *anti_sym -> *antisym*

     vector_less_eq_def -> vector_le_def

   INCOMPATIBILITY.

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

 INCOMPATIBILITY.

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

 INCOMPATIBILITY.

 *** HOLCF ***

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

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

 Instances are provided for all type constructors defined in HOLCF.

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

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

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

 recursion using previously-defined type constructors.  See

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

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

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

 simplification.  Rewriting is done using rules declared with the

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

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

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

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

 constructor are pre-configured.

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

 for mutually-recursive definitions:  Induction rules have conclusions

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

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

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

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

 as well.)

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

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

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

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

 examples.

 *** ML ***

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

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

 * Structure Name_Space (formerly NameSpace) now manages uniquely

 identified entries, with some additional information such as source

 position, logical grouping etc.

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

 modernized functors Theory_Data, Proof_Data, Generic_Data.  Data needs

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

 copy operation) is still available for some time.

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

 provides a high-level programming interface to synchronized state

 variables with atomic update.  This works via pure function

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

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

 either directly or indirectly via other synchronized variables!

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

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

 behaviour.  The Isar toplevel keeps this structure open, to

 accommodate Proof General as well as quick and dirty interactive

 experiments with references.

 * PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for

 parallel tactical reasoning.

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

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

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

 body tactic may introduce new subgoals and schematic variables.

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

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

 or Subgoal.FOCUS etc.

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

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

 separately.)  Minor INCOMPATIBILITY.

 * Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.

 * Renamed several structures FooBar to Foo_Bar.  Occasional,

 INCOMPATIBILITY.

 * Operations of structure Skip_Proof no longer require quick_and_dirty

 mode, which avoids critical setmp.

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

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

 Attrib/Method.setup introduced in Isabelle2009.

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

 back on global_simpset_of, global_claset_of, global_clasimpset_of as

 last resort.  INCOMPATIBILITY.

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

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

 or even Display.pretty_thm_without_context as last resort.

 INCOMPATIBILITY.

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

 Syntax.pretty_typ/term directly, preferably with proper context

 instead of global theory.

 *** System ***

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

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

 usedir option -q.

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

 also the system manual.

 * The isabelle makeall tool now operates on all components with

 IsaMakefile, not just hardwired "logics".

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

 this is always enabled.

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

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

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

 currently supported on Linux only.

 New in Isabelle2009 (April 2009)

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

 *** General ***

 * Simplified main Isabelle executables, with less surprises on

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

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

     "isatool."

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

     removed (should rarely occur to regular users).

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

     removed (interfaces are now regular Isabelle tools).

 Within scripts and make files, the Isabelle environment variables

 ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE,

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

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

 the interface was uninstalled or changed otherwise.  Individual

 interface tool configuration is now more explicit, see also the

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

 via "isabelle emacs".

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

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

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

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

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

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

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

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

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

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

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

 * Proofs of fully specified statements are run in parallel on

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

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

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

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

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

 as hyperlinks are now available uniformly.

 *** Pure ***

 * Complete re-implementation of locales.  INCOMPATIBILITY in several

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

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

 - In locale expressions, instantiation replaces renaming.  Parameters

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

 parameter inheritance, in locale declarations, parameters that are not

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

 with their syntax at the beginning of the for clause.

 - Syntax from abbreviations and definitions in locales is available in

 locale expressions and context elements.  The latter is particularly

 useful in locale declarations.

 - More flexible mechanisms to qualify names generated by locale

 expressions.  Qualifiers (prefixes) may be specified in locale

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

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

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

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

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

 implicit qualifiers derived from the parameter names of a locale are

 no longer generated.

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

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

 brackets) is no longer available.  Use locale expressions.

 - When converting proof scripts, mandatory qualifiers in

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

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

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

 in locale expressions range over a single locale instance only.

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

 In existing theorem specifications replace the includes element by the

 respective context elements of the included locale, omitting those

 that are already present in the theorem specification.  Multiple

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

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

 notably theorems) may be regained by interpreting the respective

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

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

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

 consider declaring a new locale with additional type constraints on

 the parameters (context element "constrains").

 - Discontinued "locale (open)".  INCOMPATIBILITY.

 - Locale interpretation commands no longer attempt to simplify goal.

 INCOMPATIBILITY: in rare situations the generated goal differs.  Use

 methods intro_locales and unfold_locales to clarify.

 - Locale interpretation commands no longer accept interpretation

 attributes.  INCOMPATIBILITY.

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

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

 in HOL, write

     class foo = ...

 instead of

     class foo = type + ...

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

 parameter prefix any longer.  INCOMPATIBILITY.

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

 INCOMPATIBILITY, use proper 'instantiation' target instead.

 * Recovered hiding of consts, which was accidentally broken in

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

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

 * Slightly more coherent Pure syntax, with updated documentation in

 isar-ref manual.  Removed locales meta_term_syntax and

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

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

 directly in regular applications.

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

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

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

 interface with 'setup' command instead.

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

 theory context.

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

 context.  INCOMPATIBILITY.

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

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

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

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

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

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

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

 The result contains an implicit sort hypotheses as before --

 SORT_CONSTRAINT premises are eliminated as part of the canonical rule

 normalization.

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

 addressing etc.

 * Changed defaults for unify configuration options:

   unify_trace_bound = 50 (formerly 25)

   unify_search_bound = 60 (formerly 30)

 * Different bookkeeping for code equations (INCOMPATIBILITY):

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

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

      parts of the code generator framework).

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

      attribute) gain priority over default code equations stemming

      from definition, primrec, fun etc.

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

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

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

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

 patterns, e.g.

     find_consts "_ => bool"

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

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

 conjunctive and queries may be negated by prefixing them with a

 hyphen:

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

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

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

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

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

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

 Cf. associated options in Proof General Isabelle settings menu,

 enabled by default, with reasonable timeout for pathological cases of

 higher-order unification.

 *** Document preparation ***

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

 demanding keyword 'by' and supporting the full method expression

 syntax just like the Isar command 'by'.

 *** HOL ***

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

 points Main and Complex_Main remain as before.

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

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

 experimentation and tool development.  Note that user applications

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

 Main, as before.

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

 experimentation due to shorter build times.

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

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

 remains valid, but theories formerly using Complex_Main should now use

 new entry point Hypercomplex.

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

 Posix processes.  Avoids potentially expensive forking of the ML

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

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

 within the theory via plain ML wrapper functions.  Basic Sledgehammer

 commands are covered in the isar-ref manual.

 * Wrapper scripts for remote SystemOnTPTP service allows to use

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

 provers may be included via suitable ML wrappers, see also

 src/HOL/ATP_Linkup.thy.

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

 menu.

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

 (contains the empty clause).

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

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

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

 src/Tools/coherent.ML).

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

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

 logically there is no difference.  INCOMPATIBILITY.

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

 result of the first successful evaluation mechanism is printed.  In

 square brackets a particular named evaluation mechanisms may be

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

 src/HOL/ex/Eval_Examples.thy.

 * Normalization by evaluation now allows non-leftlinear equations.

 Declare with attribute [code nbe].

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

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

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

 are now presented as a list of individual projections

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

 explicit HOL conjunction is no longer supported.  INCOMPATIBILITY, in

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

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

 rule: prod.exhaust) here.

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

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

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

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

 * New predicate "strict_mono" classifies strict functions on partial

 orders.  With strict functions on linear orders, reasoning about

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

 "strict_mono_less_eq" and "strict_mono_less".

 * Some set operations are now proper qualified constants with

 authentic syntax.  INCOMPATIBILITY:

     op Int ~>   Set.Int

     op Un ~>    Set.Un

     INTER ~>    Set.INTER

     UNION ~>    Set.UNION

     Inter ~>    Set.Inter

     Union ~>    Set.Union

     {} ~>       Set.empty

     UNIV ~>     Set.UNIV

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

 theory Set.

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

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

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

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

 Dense_Linear_Order) are now in directory HOL/Decision_Procs.

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

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

 interval arithmetic.  In the formulas are also the transcendental

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

 allowed. For examples see

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

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

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

 INCOMPATIBILITY.

 * Made source layout more coherent with logical distribution

 structure:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 possible), avoiding strange error messages.

 * Method "sizechange" automates termination proofs using (a

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

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

 * Simplifier: simproc for let expressions now unfolds if bound

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

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

 fast_arith_neq_limit is exceeded, instead of giving up entirely.

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

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

 proofs, e.g.

   assumes [arith]: "x > 0"

 Global usage is discouraged because of possible performance impact.

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

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

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

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

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

 INCOMPATIBILITY.

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

 induction rule "less_induct" as assumption.  For instantiation of

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

 INCOMPATIBILITY.

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

 INCOMPATIBILITY: Instantiation proofs for order, linorder

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

 preorder_class.*.

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

 "diag" to "Id_on".

 * Theory Finite_Set: added a new fold combinator of type

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

 Occasionally this is more convenient than the old fold combinator

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

 fold_image.

 * Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps"

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

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

 the former will disappear at some point.

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

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

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

 rat_power_0    -> power_0

 rat_power_Suc  -> power_Suc

 realpow_0      -> power_0

 realpow_Suc    -> power_Suc

 complexpow_0   -> power_0

 complexpow_Suc -> power_Suc

 power_poly_0   -> power_0

 power_poly_Suc -> power_Suc

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

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

 dvd has been generalized to class comm_semiring_1.  Likewise a bunch

 of lemmas from Divides has been generalized from nat to class

 semiring_div.  INCOMPATIBILITY.  This involves the following theorem

 renames resulting from duplicate elimination:

     dvd_def_mod ~>          dvd_eq_mod_eq_0

     zero_dvd_iff ~>         dvd_0_left_iff

     dvd_0 ~>                dvd_0_right

     DIVISION_BY_ZERO_DIV ~> div_by_0

     DIVISION_BY_ZERO_MOD ~> mod_by_0

     mult_div ~>             div_mult_self2_is_id

     mult_mod ~>             mod_mult_self2_is_0

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

 generalizations (from Divides and Ring_and_Field).  INCOMPATIBILITY,

 rename old lemmas as follows:

 dvd_diff               -> nat_dvd_diff

 dvd_zminus_iff         -> dvd_minus_iff

 mod_add1_eq            -> mod_add_eq

 mod_mult1_eq           -> mod_mult_right_eq

 mod_mult1_eq'          -> mod_mult_left_eq

 mod_mult_distrib_mod   -> mod_mult_eq

 nat_mod_add_left_eq    -> mod_add_left_eq

 nat_mod_add_right_eq   -> mod_add_right_eq

 nat_mod_div_trivial    -> mod_div_trivial

 nat_mod_mod_trivial    -> mod_mod_trivial

 zdiv_zadd_self1        -> div_add_self1

 zdiv_zadd_self2        -> div_add_self2

 zdiv_zmult_self1       -> div_mult_self2_is_id

 zdiv_zmult_self2       -> div_mult_self1_is_id

 zdvd_triv_left         -> dvd_triv_left

 zdvd_triv_right        -> dvd_triv_right

 zdvd_zmult_cancel_disj -> dvd_mult_cancel_left

 zmod_eq0_zdvd_iff      -> dvd_eq_mod_eq_0[symmetric]

 zmod_zadd_left_eq      -> mod_add_left_eq

 zmod_zadd_right_eq     -> mod_add_right_eq

 zmod_zadd_self1        -> mod_add_self1

 zmod_zadd_self2        -> mod_add_self2

 zmod_zadd1_eq          -> mod_add_eq

 zmod_zdiff1_eq         -> mod_diff_eq

 zmod_zdvd_zmod         -> mod_mod_cancel

 zmod_zmod_cancel       -> mod_mod_cancel

 zmod_zmult_self1       -> mod_mult_self2_is_0

 zmod_zmult_self2       -> mod_mult_self1_is_0

 zmod_1                 -> mod_by_1

 zdiv_1                 -> div_by_1

 zdvd_abs1              -> abs_dvd_iff

 zdvd_abs2              -> dvd_abs_iff

 zdvd_refl              -> dvd_refl

 zdvd_trans             -> dvd_trans

 zdvd_zadd              -> dvd_add

 zdvd_zdiff             -> dvd_diff

 zdvd_zminus_iff        -> dvd_minus_iff

 zdvd_zminus2_iff       -> minus_dvd_iff

 zdvd_zmultD            -> dvd_mult_right

 zdvd_zmultD2           -> dvd_mult_left

 zdvd_zmult_mono        -> mult_dvd_mono

 zdvd_0_right           -> dvd_0_right

 zdvd_0_left            -> dvd_0_left_iff

 zdvd_1_left            -> one_dvd

 zminus_dvd_iff         -> minus_dvd_iff

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

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

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

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

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

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

 generation is also supported, using list-style constructors.

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

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

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

 theory RealVector.

 * Theory Library/Product_Vector provides instances for the product

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

 Definitions of addition, subtraction, scalar multiplication, norms,

 and inner products are included.

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

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

 supported.

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

 first diagonalization argument.

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

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

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

 ilcm; corresponding theorems renamed accordingly.  INCOMPATIBILITY,

 may recover tupled syntax as follows:

     hide (open) const gcd

     abbreviation gcd where

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

     notation (output)

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

 The same works for lcm, zgcd, zlcm.

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

 instantiations for algebraic structures.  Removed some duplicate

 theorems.  Changes in simp rules.  INCOMPATIBILITY.

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

 corresponding code in background and inserts name of the corresponding

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

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

 simultaneously.  Provides a generic and safe interface for

 instrumentalizing code generation.  See

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

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

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

 cannot refer to constants for which user-defined serializations are

 set.  Refer to the corresponding ML counterpart directly in that

 cases.

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

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

 represented as datatype.  The characteristic theorems have to be

 proven.  INCOMPATIBILITY.  Also observe that the following theorems

 have disappeared in favour of existing ones:

     unit_induct                 ~> unit.induct

     prod_induct                 ~> prod.induct

     sum_induct                  ~> sum.induct

     Suc_Suc_eq                  ~> nat.inject

     Suc_not_Zero Zero_not_Suc   ~> nat.distinct

 *** HOL-Algebra ***

 * New locales for orders and lattices where the equivalence relation

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

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

 * New theory of factorial domains.

 * Units_l_inv and Units_r_inv are now simp rules by default.

 INCOMPATIBILITY.  Simplifier proof that require deletion of l_inv

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

 * Renamed the following theorems, INCOMPATIBILITY:

 UpperD ~> Upper_memD

 LowerD ~> Lower_memD

 least_carrier ~> least_closed

 greatest_carrier ~> greatest_closed

 greatest_Lower_above ~> greatest_Lower_below

 one_zero ~> carrier_one_zero

 one_not_zero ~> carrier_one_not_zero  (collision with assumption)

 *** HOL-Nominal ***

 * Nominal datatypes can now contain type-variables.

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

 theory targets.

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

 specification syntax now conforms to the general format as seen in

 'inductive' etc.

 * Method "perm_simp" honours the standard simplifier attributes

 (no_asm), (no_asm_use) etc.

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

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

 * Experimental command 'nominal_inductive2' derives strong induction

 principles for inductive definitions.  In contrast to

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

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

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

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

 the algorithm W:

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

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

          Gamma |- Let x be t1 in t2 : T2

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

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

 feature might be useful.  Please let us know.

 *** HOLCF ***

 * Reimplemented the simplification procedure for proving continuity

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

 continuity introduction rules with the attribute [cont2cont].

 * The continuity simproc now uses a different introduction rule for

 solving continuity subgoals on terms with lambda abstractions.  In

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

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

 Potential INCOMPATIBILITY.

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

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

 examples.  INCOMPATIBILITY.

 *** ZF ***

 * Proof of Zorn's Lemma for partial orders.

 *** ML ***

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

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

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

 5.2.1!

 * High-level support for concurrent ML programming, see

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

 particularly convenient to organize independent functional

 computations.  The concept of "synchronized variables" provides a

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

 delicate details of mutexes and condition variables.  (Requires

 Poly/ML 5.2.1 or later.)

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

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

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

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

 INCOMPATIBILITY, need to provide proper Isar context when invoking the

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

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

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

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

 a purely sequential fashion, disregarding the nested proof structure.

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

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

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

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

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

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

 Method.add_method.

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

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

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

 is specified.  INCOMPATIBILITY, need to simplify existing oracle code

 accordingly.  Note that extra performance may be gained by producing

 the cterm carefully, avoiding slow Thm.cterm_of.

 * Simplified interface for defining document antiquotations via

 ThyOutput.antiquotation, ThyOutput.output, and optionally

 ThyOutput.maybe_pretty_source.  INCOMPATIBILITY, need to simplify user

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

 examples.

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

 name space operations.  Basic operations on qualified names have been

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

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

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

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

 tracking of source positions.  INCOMPATIBILITY, need to wrap old

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

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

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

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

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

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

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

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

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

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

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

 resort for legacy applications.

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

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

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

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

 explicit runtime argument.

 * Rules and tactics that read instantiations (read_instantiate,

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

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

 the variables are specified as plain indexnames, not string encodings

 thereof.  INCOMPATIBILITY.

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

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

 for theorem dependency output of transactions resulting in a new

 theory state.

 * ML antiquotations: block-structured compilation context indicated by

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

   @{binding name}                         - basic name binding

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

   @{note name = fact}                     - fact abbreviation

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

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

   @{lemma prop by method}                 - singleton goal

   @{lemma prop by meth1 meth2}            - singleton goal

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

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

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

 *** System ***

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

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

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

 isabelle-process).  The PROOFGENERAL_HOME setting determines the

 installation location of the Proof General distribution.

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

 the Isabelle process into a JVM/Scala application.  See

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

 process wrapper has been discontinued.)

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

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

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

 user-interface components to provide detailed feedback on internal

 prover operations.

 New in Isabelle2008 (June 2008)

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

 *** General ***

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

 and updated, with formally checked references as hyperlinks.

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

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

 conflict with concurrency.  INCOMPATIBILITY, use ML within Isar which

 provides a proper context already.

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

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

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

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

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

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

 swap theory imports.

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

 INCOMPATIBILITY in identifier syntax etc.

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

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

 white space without escapes.

 * Outer syntax: string tokens may contain arbitrary character codes

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

 "foo_bar".

 *** Pure ***

 * Context-dependent token translations.  Default setup reverts locally

 fixed variables, and adds hilite markup for undeclared frees.

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

 There are three ways of invoking it:

 (1) unused_thms

      Only finds unused theorems in the current theory.

 (2) unused_thms thy_1 ... thy_n -

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

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

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

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

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

      their ancestors.

 In order to increase the readability of the list produced by

 unused_thms, theorems that have been created by a particular instance

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

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

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

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

 unused, only one theorem in the group is displayed.

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

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

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

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

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

 duplicate fact bindings, or even accidental fact duplications.  Note

 that tools may maintain dynamically scoped facts systematically, using

 PureThy.add_thms_dynamic.

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

 * Eliminated destructive theorem database, simpset, claset, and

 clasimpset.  Potential INCOMPATIBILITY, really need to observe linear

 update of theories within ML code.

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

 INCOMPATIBILITY, object-logics depending on former Pure require

 additional setup PureThy.old_appl_syntax_setup; object-logics

 depending on former CPure need to refer to Pure.

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

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

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

 INCOMPATIBILITY.

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

 * Instantiation target allows for simultaneous specification of class

 instance operations together with an instantiation proof.

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

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

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

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

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

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

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

 situations.

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

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

 proof text.

 * Isar statements: removed obsolete case "rule_context".

 INCOMPATIBILITY, better use explicit fixes/assumes.

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

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

 predicates.

 *** Document preparation ***

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

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

 obsolete thumbpdf setup (contemporary PDF viewers do this on the

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

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

 "a4paper" option (unnecessary or even intrusive).

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

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

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

 *** HOL ***

 * New primrec package.  Specification syntax conforms in style to

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

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

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

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

 primrec specifications have authentic syntax.

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

 with multithreading.

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

 theorem is now given by the attribute max_clauses.  Theorems that

 exceed this number are ignored, with a warning printed.

 * Sledgehammer no longer produces structured proofs by default. To

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

 reconstruction_modulus, reconstruction_sorts renamed

 sledgehammer_modulus, sledgehammer_sorts.  INCOMPATIBILITY.

 * Method "induct_scheme" derives user-specified induction rules

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

 out some operations that are done internally by the function package

 and makes them available separately.  See

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

 * More flexible generation of measure functions for termination

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

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

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

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

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

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

 the declared rules.

 This setup also deals with rules like 

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

 which accommodates nested datatypes that recurse through lists.

 Similar rules are predeclared for products and option types.

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

   INCOMPATIBILITIES:

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

     definitions on => and bool.

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

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

     the following theorems have been renamed:

       subset_def   -> subset_eq

       psubset_def  -> psubset_eq

       set_diff_def -> set_diff_eq

       Compl_def    -> Compl_eq

       Sup_set_def  -> Sup_set_eq

       Inf_set_def  -> Inf_set_eq

       sup_set_def  -> sup_set_eq

       inf_set_def  -> inf_set_eq

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

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

     the unknowns in the rule is a set.

   - Higher order unification and forward proofs:

     The proof pattern

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

       then have "EX S. P S" ..

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

     algorithm) and must be replaced by the pattern

       have "EX S. P S"

       proof

         show "P S" <...>

       qed

   - Calculational reasoning with subst (or similar rules):

     The proof pattern

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

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

       finally have "P T" .

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

     must be replaced by something like

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

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

       ultimately have "P T" by simp

   - Tactics or packages written in ML code:

     Code performing pattern matching on types via

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

     must be rewritten. Moreover, functions like strip_type or

     binder_types no longer return the right value when applied to a

     type of the form

       T1 => ... => Tn => U => bool

     rather than

       T1 => ... => Tn => U set

 * Merged theories Wellfounded_Recursion, Accessible_Part and

 Wellfounded_Relations to theory Wellfounded.

 * Explicit class "eq" for executable equality.  INCOMPATIBILITY.

 * Class finite no longer treats UNIV as class parameter.  Use class

 enum from theory Library/Enum instead to achieve a similar effect.

 INCOMPATIBILITY.

 * Theory List: rule list_induct2 now has explicitly named cases "Nil"

 and "Cons".  INCOMPATIBILITY.

 * HOL (and FOL): renamed variables in rules imp_elim and swap.

 Potential INCOMPATIBILITY.

 * Theory Product_Type: duplicated lemmas split_Pair_apply and

 injective_fst_snd removed, use split_eta and prod_eqI instead.

 Renamed upd_fst to apfst and upd_snd to apsnd.  INCOMPATIBILITY.

 * Theory Nat: removed redundant lemmas that merely duplicate lemmas of

 the same name in theory Orderings:

   less_trans

   less_linear

   le_imp_less_or_eq

   le_less_trans

   less_le_trans

   less_not_sym

   less_asym

 Renamed less_imp_le to less_imp_le_nat, and less_irrefl to

 less_irrefl_nat.  Potential INCOMPATIBILITY due to more general types

 and different variable names.

 * Library/Option_ord.thy: Canonical order on option type.

 * Library/RBT.thy: Red-black trees, an efficient implementation of

 finite maps.

 * Library/Countable.thy: Type class for countable types.

 * Theory Int: The representation of numerals has changed.  The infix

 operator BIT and the bit datatype with constructors B0 and B1 have

 disappeared.  INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in

 place of "x BIT bit.B0" and "y BIT bit.B1", respectively.  Theorems

 involving BIT, B0, or B1 have been renamed with "Bit0" or "Bit1"

 accordingly.

 * Theory Nat: definition of <= and < on natural numbers no longer

 depend on well-founded relations.  INCOMPATIBILITY.  Definitions

 le_def and less_def have disappeared.  Consider lemmas not_less

 [symmetric, where ?'a = nat] and less_eq [symmetric] instead.

 * Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin

 (whose purpose mainly is for various fold_set functionals) have been

 abandoned in favor of the existing algebraic classes

 ab_semigroup_mult, comm_monoid_mult, ab_semigroup_idem_mult,

 lower_semilattice (resp. upper_semilattice) and linorder.

 INCOMPATIBILITY.

 * Theory Transitive_Closure: induct and cases rules now declare proper

 case_names ("base" and "step").  INCOMPATIBILITY.

 * Theorem Inductive.lfp_ordinal_induct generalized to complete

 lattices.  The form set-specific version is available as

 Inductive.lfp_ordinal_induct_set.

 * Renamed theorems "power.simps" to "power_int.simps".

 INCOMPATIBILITY.

 * Class semiring_div provides basic abstract properties of semirings

 with division and modulo operations.  Subsumes former class dvd_mod.

 * Merged theories IntDef, Numeral and IntArith into unified theory

 Int.  INCOMPATIBILITY.

 * Theory Library/Code_Index: type "index" now represents natural

 numbers rather than integers.  INCOMPATIBILITY.

 * New class "uminus" with operation "uminus" (split of from class

 "minus" which now only has operation "minus", binary).

 INCOMPATIBILITY.

 * Constants "card", "internal_split", "option_map" now with authentic

 syntax.  INCOMPATIBILITY.

 * Definitions subset_def, psubset_def, set_diff_def, Compl_def,

 le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def,

 sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def,

 Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def,

 Sup_set_def, le_def, less_def, option_map_def now with object

 equality.  INCOMPATIBILITY.

 * Records. Removed K_record, and replaced it by pure lambda term

 %x. c. The simplifier setup is now more robust against eta expansion.

 INCOMPATIBILITY: in cases explicitly referring to K_record.

 * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}.

 * Library/ListVector: new theory of arithmetic vector operations.

 * Library/Order_Relation: new theory of various orderings as sets of

 pairs.  Defines preorders, partial orders, linear orders and

 well-orders on sets and on types.

 *** ZF ***

 * Renamed some theories to allow to loading both ZF and HOL in the

 same session:

   Datatype  -> Datatype_ZF

   Inductive -> Inductive_ZF

   Int       -> Int_ZF

   IntDiv    -> IntDiv_ZF

   Nat       -> Nat_ZF

   List      -> List_ZF

   Main      -> Main_ZF

 INCOMPATIBILITY: ZF theories that import individual theories below

 Main might need to be adapted.  Regular theory Main is still

 available, as trivial extension of Main_ZF.

 *** ML ***

 * ML within Isar: antiquotation @{const name} or @{const

 name(typargs)} produces statically-checked Const term.

 * Functor NamedThmsFun: data is available to the user as dynamic fact

 (of the same name).  Removed obsolete print command.

 * Removed obsolete "use_legacy_bindings" function.

 * The ``print mode'' is now a thread-local value derived from a global

 template (the former print_mode reference), thus access becomes

 non-critical.  The global print_mode reference is for session

 management only; user-code should use print_mode_value,

 print_mode_active, PrintMode.setmp etc.  INCOMPATIBILITY.

 * Functions system/system_out provide a robust way to invoke external

 shell commands, with propagation of interrupts (requires Poly/ML

 5.2.1).  Do not use OS.Process.system etc. from the basis library!

 *** System ***

 * Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs ---

 in accordance with Proof General 3.7, which prefers GNU emacs.

 * isatool tty runs Isabelle process with plain tty interaction;

 optional line editor may be specified via ISABELLE_LINE_EDITOR

 setting, the default settings attempt to locate "ledit" and "rlwrap".

 * isatool browser now works with Cygwin as well, using general

 "javapath" function defined in Isabelle process environment.

 * YXML notation provides a simple and efficient alternative to

 standard XML transfer syntax.  See src/Pure/General/yxml.ML and

 isatool yxml as described in the Isabelle system manual.

 * JVM class isabelle.IsabelleProcess (located in Isabelle/lib/classes)

 provides general wrapper for managing an Isabelle process in a robust

 fashion, with ``cooked'' output from stdin/stderr.

 * Rudimentary Isabelle plugin for jEdit (see Isabelle/lib/jedit),

 based on Isabelle/JVM process wrapper (see Isabelle/lib/classes).

 * Removed obsolete THIS_IS_ISABELLE_BUILD feature.  NB: the documented

 way of changing the user's settings is via

 ISABELLE_HOME_USER/etc/settings, which is a fully featured bash

 script.

 * Multithreading.max_threads := 0 refers to the number of actual CPU

 cores of the underlying machine, which is a good starting point for

 optimal performance tuning.  The corresponding usedir option -M allows

 "max" as an alias for "0".  WARNING: does not work on certain versions

 of Mac OS (with Poly/ML 5.1).

 * isabelle-process: non-ML sessions are run with "nice", to reduce the

 adverse effect of Isabelle flooding interactive front-ends (notably

 ProofGeneral / XEmacs).

 New in Isabelle2007 (November 2007)

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

 *** General ***

 * More uniform information about legacy features, notably a

 warning/error of "Legacy feature: ...", depending on the state of the

 tolerate_legacy_features flag (default true). FUTURE INCOMPATIBILITY:

 legacy features will disappear eventually.

 * Theory syntax: the header format ``theory A = B + C:'' has been

 discontinued in favour of ``theory A imports B C begin''.  Use isatool

 fixheaders to convert existing theory files.  INCOMPATIBILITY.

 * Theory syntax: the old non-Isar theory file format has been

 discontinued altogether.  Note that ML proof scripts may still be used

 with Isar theories; migration is usually quite simple with the ML

 function use_legacy_bindings.  INCOMPATIBILITY.

 * Theory syntax: some popular names (e.g. 'class', 'declaration',

 'fun', 'help', 'if') are now keywords.  INCOMPATIBILITY, use double

 quotes.

 * Theory loader: be more serious about observing the static theory

 header specifications (including optional directories), but not the

 accidental file locations of previously successful loads.  The strict

 update policy of former update_thy is now already performed by

 use_thy, so the former has been removed; use_thys updates several

 theories simultaneously, just as 'imports' within a theory header

 specification, but without merging the results.  Potential

 INCOMPATIBILITY: may need to refine theory headers and commands

 ROOT.ML which depend on load order.

 * Theory loader: optional support for content-based file

 identification, instead of the traditional scheme of full physical

 path plus date stamp; configured by the ISABELLE_FILE_IDENT setting

 (cf. the system manual).  The new scheme allows to work with

 non-finished theories in persistent session images, such that source

 files may be moved later on without requiring reloads.

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

 file (with the same base name as the theory) are considered a legacy

 feature, which will disappear eventually. Even now, the theory loader

 no longer maintains dependencies on such files.

 * Syntax: the scope for resolving ambiguities via type-inference is

 now limited to individual terms, instead of whole simultaneous

 specifications as before. This greatly reduces the complexity of the

 syntax module and improves flexibility by separating parsing and

 type-checking. INCOMPATIBILITY: additional type-constraints (explicit

 'fixes' etc.) are required in rare situations.

 * Syntax: constants introduced by new-style packages ('definition',

 'abbreviation' etc.) are passed through the syntax module in

 ``authentic mode''. This means that associated mixfix annotations

 really stick to such constants, independently of potential name space

 ambiguities introduced later on. INCOMPATIBILITY: constants in parse

 trees are represented slightly differently, may need to adapt syntax

 translations accordingly. Use CONST marker in 'translations' and

 @{const_syntax} antiquotation in 'parse_translation' etc.

 * Legacy goal package: reduced interface to the bare minimum required

 to keep existing proof scripts running.  Most other user-level

 functions are now part of the OldGoals structure, which is *not* open

 by default (consider isatool expandshort before open OldGoals).

 Removed top_sg, prin, printyp, pprint_term/typ altogether, because

 these tend to cause confusion about the actual goal (!) context being

 used here, which is not necessarily the same as the_context().

 * Command 'find_theorems': supports "*" wild-card in "name:"

 criterion; "with_dups" option.  Certain ProofGeneral versions might

 support a specific search form (see ProofGeneral/CHANGES).

 * The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1

 by default, which means that "prems" (and also "fixed variables") are

 suppressed from proof state output.  Note that the ProofGeneral

 settings mechanism allows to change and save options persistently, but

 older versions of Isabelle will fail to start up if a negative prems

 limit is imposed.

 * Local theory targets may be specified by non-nested blocks of

 ``context/locale/class ... begin'' followed by ``end''.  The body may

 contain definitions, theorems etc., including any derived mechanism

 that has been implemented on top of these primitives.  This concept

 generalizes the existing ``theorem (in ...)'' towards more versatility

 and scalability.

 * Proof General interface: proper undo of final 'end' command;

 discontinued Isabelle/classic mode (ML proof scripts).

 *** Document preparation ***

 * Added antiquotation @{theory name} which prints the given name,

 after checking that it refers to a valid ancestor theory in the

 current context.

 * Added antiquotations @{ML_type text} and @{ML_struct text} which

 check the given source text as ML type/structure, printing verbatim.

 * Added antiquotation @{abbrev "c args"} which prints the abbreviation

 "c args == rhs" given in the current context.  (Any number of

 arguments may be given on the LHS.)

 *** Pure ***

 * The 'class' package offers a combination of axclass and locale to

 achieve Haskell-like type classes in Isabelle.  Definitions and

 theorems within a class context produce both relative results (with

 implicit parameters according to the locale context), and polymorphic

 constants with qualified polymorphism (according to the class

 context).  Within the body context of a 'class' target, a separate

 syntax layer ("user space type system") takes care of converting

 between global polymorphic consts and internal locale representation.

 See src/HOL/ex/Classpackage.thy for examples (as well as main HOL).

 "isatool doc classes" provides a tutorial.

 * Generic code generator framework allows to generate executable

 code for ML and Haskell (including Isabelle classes).  A short usage

 sketch:

     internal compilation:

         export_code <list of constants (term syntax)> in SML

     writing SML code to a file:

         export_code <list of constants (term syntax)> in SML <filename>

     writing OCaml code to a file:

         export_code <list of constants (term syntax)> in OCaml <filename>

     writing Haskell code to a bunch of files:

         export_code <list of constants (term syntax)> in Haskell <filename>

     evaluating closed propositions to True/False using code generation:

         method ``eval''

 Reasonable default setup of framework in HOL.

 Theorem attributs for selecting and transforming function equations theorems:

     [code fun]:        select a theorem as function equation for a specific constant

     [code fun del]:    deselect a theorem as function equation for a specific constant

     [code inline]:     select an equation theorem for unfolding (inlining) in place

     [code inline del]: deselect an equation theorem for unfolding (inlining) in place

 User-defined serializations (target in {SML, OCaml, Haskell}):

     code_const <and-list of constants (term syntax)>

       {(target) <and-list of const target syntax>}+

     code_type <and-list of type constructors>

       {(target) <and-list of type target syntax>}+

     code_instance <and-list of instances>

       {(target)}+

         where instance ::= <type constructor> :: <class>

     code_class <and_list of classes>

       {(target) <and-list of class target syntax>}+

         where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?

 code_instance and code_class only are effective to target Haskell.

 For example usage see src/HOL/ex/Codegenerator.thy and

 src/HOL/ex/Codegenerator_Pretty.thy.  A separate tutorial on code

 generation from Isabelle/HOL theories is available via "isatool doc

 codegen".

 * Code generator: consts in 'consts_code' Isar commands are now

 referred to by usual term syntax (including optional type

 annotations).

 * Command 'no_translations' removes translation rules from theory

 syntax.

 * Overloaded definitions are now actually checked for acyclic

 dependencies.  The overloading scheme is slightly more general than

 that of Haskell98, although Isabelle does not demand an exact

 correspondence to type class and instance declarations.

 INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more

 exotic versions of overloading -- at the discretion of the user!

 Polymorphic constants are represented via type arguments, i.e. the

 instantiation that matches an instance against the most general

 declaration given in the signature.  For example, with the declaration

 c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented

 as c(nat).  Overloading is essentially simultaneous structural

 recursion over such type arguments.  Incomplete specification patterns

 impose global constraints on all occurrences, e.g. c('a * 'a) on the

 LHS means that more general c('a * 'b) will be disallowed on any RHS.

 Command 'print_theory' outputs the normalized system of recursive

 equations, see section "definitions".

 * Configuration options are maintained within the theory or proof

 context (with name and type bool/int/string), providing a very simple

 interface to a poor-man's version of general context data.  Tools may

 declare options in ML (e.g. using Attrib.config_int) and then refer to

 these values using Config.get etc.  Users may change options via an

 associated attribute of the same name.  This form of context

 declaration works particularly well with commands 'declare' or

 'using', for example ``declare [[foo = 42]]''.  Thus it has become

 very easy to avoid global references, which would not observe Isar

 toplevel undo/redo and fail to work with multithreading.

 Various global ML references of Pure and HOL have been turned into

 configuration options:

   Unify.search_bound		unify_search_bound

   Unify.trace_bound		unify_trace_bound

   Unify.trace_simp		unify_trace_simp

   Unify.trace_types		unify_trace_types

   Simplifier.simp_depth_limit	simp_depth_limit

   Blast.depth_limit		blast_depth_limit

   DatatypeProp.dtK		datatype_distinctness_limit

   fast_arith_neq_limit  	fast_arith_neq_limit

   fast_arith_split_limit	fast_arith_split_limit

 * Named collections of theorems may be easily installed as context

 data using the functor NamedThmsFun (see also

 src/Pure/Tools/named_thms.ML).  The user may add or delete facts via

 attributes; there is also a toplevel print command.  This facility is

 just a common case of general context data, which is the preferred way

 for anything more complex than just a list of facts in canonical

 order.

 * Isar: command 'declaration' augments a local theory by generic

 declaration functions written in ML.  This enables arbitrary content

 being added to the context, depending on a morphism that tells the

 difference of the original declaration context wrt. the application

 context encountered later on.

 * Isar: proper interfaces for simplification procedures.  Command

 'simproc_setup' declares named simprocs (with match patterns, and body

 text in ML).  Attribute "simproc" adds/deletes simprocs in the current

 context.  ML antiquotation @{simproc name} retrieves named simprocs.

 * Isar: an extra pair of brackets around attribute declarations

 abbreviates a theorem reference involving an internal dummy fact,

 which will be ignored later --- only the effect of the attribute on

 the background context will persist.  This form of in-place

 declarations is particularly useful with commands like 'declare' and

 'using', for example ``have A using [[simproc a]] by simp''.

 * Isar: method "assumption" (and implicit closing of subproofs) now

 takes simple non-atomic goal assumptions into account: after applying

 an assumption as a rule the resulting subgoals are solved by atomic

 assumption steps.  This is particularly useful to finish 'obtain'

 goals, such as "!!x. (!!x. P x ==> thesis) ==> P x ==> thesis",

 without referring to the original premise "!!x. P x ==> thesis" in the

 Isar proof context.  POTENTIAL INCOMPATIBILITY: method "assumption" is

 more permissive.

 * Isar: implicit use of prems from the Isar proof context is

 considered a legacy feature.  Common applications like ``have A .''

 may be replaced by ``have A by fact'' or ``note `A`''.  In general,

 referencing facts explicitly here improves readability and

 maintainability of proof texts.

 * Isar: improper proof element 'guess' is like 'obtain', but derives

 the obtained context from the course of reasoning!  For example:

   assume "EX x y. A x & B y"   -- "any previous fact"

   then guess x and y by clarify

 This technique is potentially adventurous, depending on the facts and

 proof tools being involved here.

 * Isar: known facts from the proof context may be specified as literal

 propositions, using ASCII back-quote syntax.  This works wherever

 named facts used to be allowed so far, in proof commands, proof

 methods, attributes etc.  Literal facts are retrieved from the context

 according to unification of type and term parameters.  For example,

 provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known

 theorems in the current context, then these are valid literal facts:

 `A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc.

 There is also a proof method "fact" which does the same composition

 for explicit goal states, e.g. the following proof texts coincide with

 certain special cases of literal facts:

   have "A" by fact                 ==  note `A`

   have "A ==> B" by fact           ==  note `A ==> B`

   have "!!x. P x ==> Q x" by fact  ==  note `!!x. P x ==> Q x`

   have "P a ==> Q a" by fact       ==  note `P a ==> Q a`

 * Isar: ":" (colon) is no longer a symbolic identifier character in

 outer syntax.  Thus symbolic identifiers may be used without

 additional white space in declarations like this: ``assume *: A''.

 * Isar: 'print_facts' prints all local facts of the current context,

 both named and unnamed ones.

 * Isar: 'def' now admits simultaneous definitions, e.g.:

   def x == "t" and y == "u"

 * Isar: added command 'unfolding', which is structurally similar to

 'using', but affects both the goal state and facts by unfolding given

 rewrite rules.  Thus many occurrences of the 'unfold' method or

 'unfolded' attribute may be replaced by first-class proof text.

 * Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded',

 and command 'unfolding' now all support object-level equalities

 (potentially conditional).  The underlying notion of rewrite rule is

 analogous to the 'rule_format' attribute, but *not* that of the

 Simplifier (which is usually more generous).

 * Isar: the new attribute [rotated n] (default n = 1) rotates the

 premises of a theorem by n. Useful in conjunction with drule.

 * Isar: the goal restriction operator [N] (default N = 1) evaluates a

 method expression within a sandbox consisting of the first N

 sub-goals, which need to exist.  For example, ``simp_all [3]''

 simplifies the first three sub-goals, while (rule foo, simp_all)[]

 simplifies all new goals that emerge from applying rule foo to the

 originally first one.

 * Isar: schematic goals are no longer restricted to higher-order

 patterns; e.g. ``lemma "?P(?x)" by (rule TrueI)'' now works as

 expected.

 * Isar: the conclusion of a long theorem statement is now either

 'shows' (a simultaneous conjunction, as before), or 'obtains'

 (essentially a disjunction of cases with local parameters and

 assumptions).  The latter allows to express general elimination rules

 adequately; in this notation common elimination rules look like this:

   lemma exE:    -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis"

     assumes "EX x. P x"

     obtains x where "P x"

   lemma conjE:  -- "A & B ==> (A ==> B ==> thesis) ==> thesis"

     assumes "A & B"

     obtains A and B

   lemma disjE:  -- "A | B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis"

     assumes "A | B"

     obtains

       A

     | B

 The subsequent classical rules even refer to the formal "thesis"

 explicitly:

   lemma classical:     -- "(~ thesis ==> thesis) ==> thesis"

     obtains "~ thesis"

   lemma Peirce's_Law:  -- "((thesis ==> something) ==> thesis) ==> thesis"

     obtains "thesis ==> something"

 The actual proof of an 'obtains' statement is analogous to that of the

 Isar proof element 'obtain', only that there may be several cases.

 Optional case names may be specified in parentheses; these will be

 available both in the present proof and as annotations in the

 resulting rule, for later use with the 'cases' method (cf. attribute

 case_names).

 * Isar: the assumptions of a long theorem statement are available as

 "assms" fact in the proof context.  This is more appropriate than the

 (historical) "prems", which refers to all assumptions of the current

 context, including those from the target locale, proof body etc.

 * Isar: 'print_statement' prints theorems from the current theory or

 proof context in long statement form, according to the syntax of a

 top-level lemma.

 * Isar: 'obtain' takes an optional case name for the local context

 introduction rule (default "that").

 * Isar: removed obsolete 'concl is' patterns.  INCOMPATIBILITY, use

 explicit (is "_ ==> ?foo") in the rare cases where this still happens

 to occur.

 * Pure: syntax "CONST name" produces a fully internalized constant

 according to the current context.  This is particularly useful for

 syntax translations that should refer to internal constant

 representations independently of name spaces.

 * Pure: syntax constant for foo (binder "FOO ") is called "foo_binder"

 instead of "FOO ". This allows multiple binder declarations to coexist

 in the same context.  INCOMPATIBILITY.

 * Isar/locales: 'notation' provides a robust interface to the 'syntax'

 primitive that also works in a locale context (both for constants and

 fixed variables). Type declaration and internal syntactic representation

 of given constants retrieved from the context. Likewise, the

 'no_notation' command allows to remove given syntax annotations from the

 current context.

 * Isar/locales: new derived specification elements 'axiomatization',

 'definition', 'abbreviation', which support type-inference, admit

 object-level specifications (equality, equivalence).  See also the

 isar-ref manual.  Examples:

   axiomatization

     eq  (infix "===" 50) where

     eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"

   definition "f x y = x + y + 1"

   definition g where "g x = f x x"

   abbreviation

     neq  (infix "=!=" 50) where

     "x =!= y == ~ (x === y)"

 These specifications may be also used in a locale context.  Then the

 constants being introduced depend on certain fixed parameters, and the

 constant name is qualified by the locale base name.  An internal

 abbreviation takes care for convenient input and output, making the

 parameters implicit and using the original short name.  See also

 src/HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic

 entities from a monomorphic theory.

 Presently, abbreviations are only available 'in' a target locale, but

 not inherited by general import expressions.  Also note that

 'abbreviation' may be used as a type-safe replacement for 'syntax' +

 'translations' in common applications.  The "no_abbrevs" print mode

 prevents folding of abbreviations in term output.

 Concrete syntax is attached to specified constants in internal form,

 independently of name spaces.  The parse tree representation is

 slightly different -- use 'notation' instead of raw 'syntax', and

 'translations' with explicit "CONST" markup to accommodate this.

 * Pure/Isar: unified syntax for new-style specification mechanisms

 (e.g.  'definition', 'abbreviation', or 'inductive' in HOL) admits

 full type inference and dummy patterns ("_").  For example:

   definition "K x _ = x"

   inductive conj for A B

   where "A ==> B ==> conj A B"

 * Pure: command 'print_abbrevs' prints all constant abbreviations of

 the current context.  Print mode "no_abbrevs" prevents inversion of

 abbreviations on output.

 * Isar/locales: improved parameter handling: use of locales "var" and

 "struct" no longer necessary; - parameter renamings are no longer

 required to be injective.  For example, this allows to define

 endomorphisms as locale endom = homom mult mult h.

 * Isar/locales: changed the way locales with predicates are defined.

 Instead of accumulating the specification, the imported expression is

 now an interpretation.  INCOMPATIBILITY: different normal form of

 locale expressions.  In particular, in interpretations of locales with

 predicates, goals repesenting already interpreted fragments are not

 removed automatically.  Use methods `intro_locales' and

 `unfold_locales'; see below.

 * Isar/locales: new methods `intro_locales' and `unfold_locales'

 provide backward reasoning on locales predicates.  The methods are

 aware of interpretations and discharge corresponding goals.

 `intro_locales' is less aggressive then `unfold_locales' and does not

 unfold predicates to assumptions.

 * Isar/locales: the order in which locale fragments are accumulated

 has changed.  This enables to override declarations from fragments due

 to interpretations -- for example, unwanted simp rules.

 * Isar/locales: interpretation in theories and proof contexts has been

 extended.  One may now specify (and prove) equations, which are

 unfolded in interpreted theorems.  This is useful for replacing

 defined concepts (constants depending on locale parameters) by

 concepts already existing in the target context.  Example:

   interpretation partial_order ["op <= :: [int, int] => bool"]

     where "partial_order.less (op <=) (x::int) y = (x < y)"

 Typically, the constant `partial_order.less' is created by a

 definition specification element in the context of locale

 partial_order.

 * Method "induct": improved internal context management to support

 local fixes and defines on-the-fly. Thus explicit meta-level

 connectives !!  and ==> are rarely required anymore in inductive goals

 (using object-logic connectives for this purpose has been long

 obsolete anyway). Common proof patterns are explained in