NEWS

more NEWS;
tuned;

Isabelle NEWS -- history user-relevant changes
==============================================

New in Isabelle2009-2 (June 2010)
---------------------------------

*** General ***

* Authentic syntax for *all* logical entities (type classes, type
constructors, term constants): provides simple and robust
correspondence between formal entities and concrete syntax.  Within
the parse tree / AST representations, "constants" are decorated by
their category (class, type, const) and spelled out explicitly with
their full internal name.

Substantial INCOMPATIBILITY concerning low-level syntax declarations
and translations (translation rules and translation functions in ML).
Some hints on upgrading:

  - Many existing uses of 'syntax' and 'translations' can be replaced
    by more modern 'type_notation', 'notation' and 'abbreviation',
    which are independent of this issue.

  - 'translations' require markup within the AST; the term syntax
    provides the following special forms:

      CONST c   -- produces syntax version of constant c from context
      XCONST c  -- literally c, checked as constant from context
      c         -- literally c, if declared by 'syntax'

    Plain identifiers are treated as AST variables -- occasionally the
    system indicates accidental variables via the error "rhs contains
    extra variables".

    Type classes and type constructors are marked according to their
    concrete syntax.  Some old translations rules need to be written
    for the "type" category, using type constructor application
    instead of pseudo-term application of the default category
    "logic".

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

      @{class_syntax c}   -- type class c within parse tree / AST
      @{term_syntax c}    -- type constructor c within parse tree / AST
      @{const_syntax c}   -- ML version of "CONST c" above
      @{syntax_const c}   -- literally c (checked wrt. 'syntax' declarations)

  - Literal types within 'typed_print_translations', i.e. those *not*
    represented as pseudo-terms are represented verbatim.  Use @{class
    c} or @{type_name c} here instead of the above syntax
    antiquotations.

Note that old non-authentic syntax was based on unqualified base
names, so all of the above "constant" names would coincide.  Recall
that 'print_syntax' and ML_command "set Syntax.trace_ast" help to
diagnose syntax problems.

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

* Concrete syntax may be attached to local entities without a proof
body, too.  This works via regular mixfix annotations for 'fix',
'def', 'obtain' etc. or via the explicit 'write' command, which is
similar to the 'notation' command in theory specifications.

* Discontinued unnamed infix syntax (legacy feature for many years) --
need to specify constant name and syntax separately.  Internal ML
datatype constructors have been renamed from InfixName to Infix etc.
Minor INCOMPATIBILITY.

* Schematic theorem statements need to be explicitly markup as such,
via commands 'schematic_lemma', 'schematic_theorem',
'schematic_corollary'.  Thus the relevance of the proof is made
syntactically clear, which impacts performance in a parallel or
asynchronous interactive environment.  Minor INCOMPATIBILITY.

* Use of cumulative prems via "!" in some proof methods has been
discontinued (old legacy feature).

* References 'trace_simp' and 'debug_simp' have been replaced by
configuration options stored in the context. Enabling tracing (the
case of debugging is similar) in proofs works via

  using [[trace_simp = true]]

Tracing is then active for all invocations of the simplifier in
subsequent goal refinement steps. Tracing may also still be enabled or
disabled via the ProofGeneral settings menu.

* Separate commands 'hide_class', 'hide_type', 'hide_const',
'hide_fact' replace the former 'hide' KIND command.  Minor
INCOMPATIBILITY.

* Improved parallelism of proof term normalization: usedir -p2 -q0 is
more efficient than combinations with -q1 or -q2.


*** Pure ***

* Proofterms record type-class reasoning explicitly, using the
"unconstrain" operation internally.  This eliminates all sort
constraints from a theorem and proof, introducing explicit
OFCLASS-premises.  On the proof term level, this operation is
automatically applied at theorem boundaries, such that closed proofs
are always free of sort constraints.  INCOMPATIBILITY for tools that
inspect proof terms.

* Local theory specifications may depend on extra type variables that
are not present in the result type -- arguments TYPE('a) :: 'a itself
are added internally.  For example:

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

* Predicates of locales introduced by classes carry a mandatory
"class" prefix.  INCOMPATIBILITY.

* Vacuous class specifications observe default sort.  INCOMPATIBILITY.

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

* Command 'code_reflect' allows to incorporate generated ML code into
runtime environment; replaces immature code_datatype antiquotation.
INCOMPATIBILITY.

* Code generator: simple concept for abstract datatypes obeying
invariants.

* Code generator: details of internal data cache have no impact on the
user space functionality any longer.

* Methods "unfold_locales" and "intro_locales" ignore non-locale
subgoals.  This is more appropriate for interpretations with 'where'.
INCOMPATIBILITY.

* Command 'example_proof' opens an empty proof body.  This allows to
experiment with Isar, without producing any persistent result.

* Commands 'type_notation' and 'no_type_notation' declare type syntax
within a local theory context, with explicit checking of the
constructors involved (in contrast to the raw 'syntax' versions).

* Commands 'types' and 'typedecl' now work within a local theory
context -- without introducing dependencies on parameters or
assumptions, which is not possible in Isabelle/Pure.

* Command 'defaultsort' has been renamed to 'default_sort', it works
within a local theory context.  Minor INCOMPATIBILITY.


*** HOL ***

* Command 'typedef' now works within a local theory context -- without
introducing dependencies on parameters or assumptions, which is not
possible in Isabelle/Pure/HOL.  Note that the logical environment may
contain multiple interpretations of local typedefs (with different
non-emptiness proofs), even in a global theory context.

* New package for quotient types.  Commands 'quotient_type' and
'quotient_definition' may be used for defining types and constants by
quotient constructions.  An example is the type of integers created by
quotienting pairs of natural numbers:
  
  fun
    intrel :: "(nat * nat) => (nat * nat) => bool" 
  where
    "intrel (x, y) (u, v) = (x + v = u + y)"

  quotient_type int = "nat × nat" / intrel
    by (auto simp add: equivp_def expand_fun_eq)
  
  quotient_definition
    "0::int" is "(0::nat, 0::nat)"

The method "lifting" can be used to lift of theorems from the
underlying "raw" type to the quotient type.  The example
src/HOL/Quotient_Examples/FSet.thy includes such a quotient
construction and provides a reasoning infrastructure for finite sets.

* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid
clash with new theory Quotient in Main HOL.

* Moved the SMT binding into the main HOL session, eliminating
separate HOL-SMT session.

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

* Theory Library/Word.thy has been removed.  Use library Word/Word.thy
for future developements; former Library/Word.thy is still present in
the AFP entry RSAPPS.

* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
longer shadowed.  INCOMPATIBILITY.

* Dropped theorem duplicate comp_arith; use semiring_norm instead.
INCOMPATIBILITY.

* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
INCOMPATIBILITY.

* Dropped normalizing_semiring etc; use the facts in semiring classes
instead.  INCOMPATIBILITY.

* Dropped several real-specific versions of lemmas about floor and
ceiling; use the generic lemmas from theory "Archimedean_Field"
instead.  INCOMPATIBILITY.

  floor_number_of_eq         ~> floor_number_of
  le_floor_eq_number_of      ~> number_of_le_floor
  le_floor_eq_zero           ~> zero_le_floor
  le_floor_eq_one            ~> one_le_floor
  floor_less_eq_number_of    ~> floor_less_number_of
  floor_less_eq_zero         ~> floor_less_zero
  floor_less_eq_one          ~> floor_less_one
  less_floor_eq_number_of    ~> number_of_less_floor
  less_floor_eq_zero         ~> zero_less_floor
  less_floor_eq_one          ~> one_less_floor
  floor_le_eq_number_of      ~> floor_le_number_of
  floor_le_eq_zero           ~> floor_le_zero
  floor_le_eq_one            ~> floor_le_one
  floor_subtract_number_of   ~> floor_diff_number_of
  floor_subtract_one         ~> floor_diff_one
  ceiling_number_of_eq       ~> ceiling_number_of
  ceiling_le_eq_number_of    ~> ceiling_le_number_of
  ceiling_le_zero_eq         ~> ceiling_le_zero
  ceiling_le_eq_one          ~> ceiling_le_one
  less_ceiling_eq_number_of  ~> number_of_less_ceiling
  less_ceiling_eq_zero       ~> zero_less_ceiling
  less_ceiling_eq_one        ~> one_less_ceiling
  ceiling_less_eq_number_of  ~> ceiling_less_number_of
  ceiling_less_eq_zero       ~> ceiling_less_zero
  ceiling_less_eq_one        ~> ceiling_less_one
  le_ceiling_eq_number_of    ~> number_of_le_ceiling
  le_ceiling_eq_zero         ~> zero_le_ceiling
  le_ceiling_eq_one          ~> one_le_ceiling
  ceiling_subtract_number_of ~> ceiling_diff_number_of
  ceiling_subtract_one       ~> ceiling_diff_one

* Theory "Finite_Set": various folding_XXX locales facilitate the
application of the various fold combinators on finite sets.

* Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"
provides abstract red-black tree type which is backed by "RBT_Impl" as
implementation.  INCOMPATIBILTY.

* Theory Library/Coinductive_List has been removed -- superseded by
AFP/thys/Coinductive.

* Theory PReal, including the type "preal" and related operations, has
been removed.  INCOMPATIBILITY.

* Split off theory "Big_Operators" containing setsum, setprod,
Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.

* Theory "Rational" renamed to "Rat", for consistency with "Nat",
"Int" etc.  INCOMPATIBILITY.

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

* New set of rules "ac_simps" provides combined assoc / commute
rewrites for all interpretations of the appropriate generic locales.

* Renamed theory "OrderedGroup" to "Groups" and split theory
"Ring_and_Field" into theories "Rings" and "Fields"; for more
appropriate and more consistent names suitable for name prefixes
within the HOL theories.  INCOMPATIBILITY.

* Some generic constants have been put to appropriate theories:
  - less_eq, less: Orderings
  - zero, one, plus, minus, uminus, times, abs, sgn: Groups
  - inverse, divide: Rings
INCOMPATIBILITY.

* More consistent naming of type classes involving orderings (and
lattices):

    lower_semilattice                   ~> semilattice_inf
    upper_semilattice                   ~> semilattice_sup

    dense_linear_order                  ~> dense_linorder

    pordered_ab_group_add               ~> ordered_ab_group_add
    pordered_ab_group_add_abs           ~> ordered_ab_group_add_abs
    pordered_ab_semigroup_add           ~> ordered_ab_semigroup_add
    pordered_ab_semigroup_add_imp_le    ~> ordered_ab_semigroup_add_imp_le
    pordered_cancel_ab_semigroup_add    ~> ordered_cancel_ab_semigroup_add
    pordered_cancel_comm_semiring       ~> ordered_cancel_comm_semiring
    pordered_cancel_semiring            ~> ordered_cancel_semiring
    pordered_comm_monoid_add            ~> ordered_comm_monoid_add
    pordered_comm_ring                  ~> ordered_comm_ring
    pordered_comm_semiring              ~> ordered_comm_semiring
    pordered_ring                       ~> ordered_ring
    pordered_ring_abs                   ~> ordered_ring_abs
    pordered_semiring                   ~> ordered_semiring

    ordered_ab_group_add                ~> linordered_ab_group_add
    ordered_ab_semigroup_add            ~> linordered_ab_semigroup_add
    ordered_cancel_ab_semigroup_add     ~> linordered_cancel_ab_semigroup_add
    ordered_comm_semiring_strict        ~> linordered_comm_semiring_strict
    ordered_field                       ~> linordered_field
    ordered_field_no_lb                 ~> linordered_field_no_lb
    ordered_field_no_ub                 ~> linordered_field_no_ub
    ordered_field_dense_linear_order    ~> dense_linordered_field
    ordered_idom                        ~> linordered_idom
    ordered_ring                        ~> linordered_ring
    ordered_ring_le_cancel_factor       ~> linordered_ring_le_cancel_factor
    ordered_ring_less_cancel_factor     ~> linordered_ring_less_cancel_factor
    ordered_ring_strict                 ~> linordered_ring_strict
    ordered_semidom                     ~> linordered_semidom
    ordered_semiring                    ~> linordered_semiring
    ordered_semiring_1                  ~> linordered_semiring_1
    ordered_semiring_1_strict           ~> linordered_semiring_1_strict
    ordered_semiring_strict             ~> linordered_semiring_strict

  The following slightly odd type classes have been moved to a
  separate theory Library/Lattice_Algebras:

    lordered_ab_group_add               ~> lattice_ab_group_add
    lordered_ab_group_add_abs           ~> lattice_ab_group_add_abs
    lordered_ab_group_add_meet          ~> semilattice_inf_ab_group_add
    lordered_ab_group_add_join          ~> semilattice_sup_ab_group_add
    lordered_ring                       ~> lattice_ring

INCOMPATIBILITY.

* Refined field classes:
  - classes division_ring_inverse_zero, field_inverse_zero,
    linordered_field_inverse_zero include rule inverse 0 = 0 --
    subsumes former division_by_zero class;
  - numerous lemmas have been ported from field to division_ring.
INCOMPATIBILITY.

* Refined algebra theorem collections:
  - dropped theorem group group_simps, use algebra_simps instead;
  - dropped theorem group ring_simps, use field_simps instead;
  - proper theorem collection field_simps subsumes former theorem
    groups field_eq_simps and field_simps;
  - dropped lemma eq_minus_self_iff which is a duplicate for
    equal_neg_zero.
INCOMPATIBILITY.

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

  fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf
  fun_left_comm_idem_union      ~> fun_left_comm_idem_sup
  inter_Inter_fold_inter        ~> inf_Inf_fold_inf
  union_Union_fold_union        ~> sup_Sup_fold_sup
  Inter_fold_inter              ~> Inf_fold_inf
  Union_fold_union              ~> Sup_fold_sup
  inter_INTER_fold_inter        ~> inf_INFI_fold_inf
  union_UNION_fold_union        ~> sup_SUPR_fold_sup
  INTER_fold_inter              ~> INFI_fold_inf
  UNION_fold_union              ~> SUPR_fold_sup

* Theory "Complete_Lattice": lemmas top_def and bot_def have been
replaced by the more convenient lemmas Inf_empty and Sup_empty.
Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace
former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right
subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.

* Reorganized theory Multiset: swapped notation of pointwise and
multiset order:

  - pointwise ordering is instance of class order with standard syntax
    <= and <;
  - multiset ordering has syntax <=# and <#; partial order properties
    are provided by means of interpretation with prefix
    multiset_order;
  - less duplication, less historical organization of sections,
    conversion from associations lists to multisets, rudimentary code
    generation;
  - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
    if needed.

Renamed:

  multiset_eq_conv_count_eq  ~>  multiset_ext_iff
  multi_count_ext  ~>  multiset_ext
  diff_union_inverse2  ~>  diff_union_cancelR

INCOMPATIBILITY.

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

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

* Theory List: added transpose.

* Library/Nat_Bijection.thy is a collection of bijective functions
between nat and other types, which supersedes the older libraries
Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy.  INCOMPATIBILITY.

  Constants:
  Nat_Int_Bij.nat2_to_nat         ~> prod_encode
  Nat_Int_Bij.nat_to_nat2         ~> prod_decode
  Nat_Int_Bij.int_to_nat_bij      ~> int_encode
  Nat_Int_Bij.nat_to_int_bij      ~> int_decode
  Countable.pair_encode           ~> prod_encode
  NatIso.prod2nat                 ~> prod_encode
  NatIso.nat2prod                 ~> prod_decode
  NatIso.sum2nat                  ~> sum_encode
  NatIso.nat2sum                  ~> sum_decode
  NatIso.list2nat                 ~> list_encode
  NatIso.nat2list                 ~> list_decode
  NatIso.set2nat                  ~> set_encode
  NatIso.nat2set                  ~> set_decode

  Lemmas:
  Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_decode
  Nat_Int_Bij.nat2_to_nat_inj     ~> inj_prod_encode
  Nat_Int_Bij.nat2_to_nat_surj    ~> surj_prod_encode
  Nat_Int_Bij.nat_to_nat2_inj     ~> inj_prod_decode
  Nat_Int_Bij.nat_to_nat2_surj    ~> surj_prod_decode
  Nat_Int_Bij.i2n_n2i_id          ~> int_encode_inverse
  Nat_Int_Bij.n2i_i2n_id          ~> int_decode_inverse
  Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode
  Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode
  Nat_Int_Bij.inj_nat_to_int_bij  ~> inj_int_encode
  Nat_Int_Bij.inj_int_to_nat_bij  ~> inj_int_decode
  Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode
  Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode

* Sledgehammer:
  - Renamed ATP commands:
    atp_info     ~> sledgehammer running_atps
    atp_kill     ~> sledgehammer kill_atps
    atp_messages ~> sledgehammer messages
    atp_minimize ~> sledgehammer minimize
    print_atps   ~> sledgehammer available_atps
    INCOMPATIBILITY.
  - Added user's manual ("isabelle doc sledgehammer").
  - Added option syntax and "sledgehammer_params" to customize
    Sledgehammer's behavior.  See the manual for details.
  - Modified the Isar proof reconstruction code so that it produces
    direct proofs rather than proofs by contradiction.  (This feature
    is still experimental.)
  - Made Isar proof reconstruction work for SPASS, remote ATPs, and in
    full-typed mode.
  - Added support for TPTP syntax for SPASS via the "spass_tptp" ATP.

* Nitpick:
  - Added and implemented "binary_ints" and "bits" options.
  - Added "std" option and implemented support for nonstandard models.
  - Added and implemented "finitize" option to improve the precision
    of infinite datatypes based on a monotonicity analysis.
  - Added support for quotient types.
  - Added support for "specification" and "ax_specification"
    constructs.
  - Added support for local definitions (for "function" and
    "termination" proofs).
  - Added support for term postprocessors.
  - Optimized "Multiset.multiset" and "FinFun.finfun".
  - Improved efficiency of "destroy_constrs" optimization.
  - Fixed soundness bugs related to "destroy_constrs" optimization and
    record getters.
  - Fixed soundness bug related to higher-order constructors.
  - Fixed soundness bug when "full_descrs" is enabled.
  - Improved precision of set constructs.
  - Added "atoms" option.
  - Added cache to speed up repeated Kodkod invocations on the same
    problems.
  - Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and
    "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and
    "SAT4J_Light".  INCOMPATIBILITY.
  - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
    "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.
  - Removed "nitpick_intro" attribute.  INCOMPATIBILITY.


*** HOLCF ***

* Variable names in lemmas generated by the domain package have
changed; the naming scheme is now consistent with the HOL datatype
package.  Some proof scripts may be affected, INCOMPATIBILITY.

* The domain package no longer defines the function "foo_copy" for
recursive domain "foo".  The reach lemma is now stated directly in
terms of "foo_take".  Lemmas and proofs that mention "foo_copy" must
be reformulated in terms of "foo_take", INCOMPATIBILITY.

* Most definedness lemmas generated by the domain package (previously
of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form
like "foo$x = UU <-> x = UU", which works better as a simp rule.
Proofs that used definedness lemmas as intro rules may break,
potential INCOMPATIBILITY.

* Induction and casedist rules generated by the domain package now
declare proper case_names (one called "bottom", and one named for each
constructor).  INCOMPATIBILITY.

* For mutually-recursive domains, separate "reach" and "take_lemma"
rules are generated for each domain, INCOMPATIBILITY.

  foo_bar.reach       ~> foo.reach  bar.reach
  foo_bar.take_lemmas ~> foo.take_lemma  bar.take_lemma

* Some lemmas generated by the domain package have been renamed for
consistency with the datatype package, INCOMPATIBILITY.

  foo.ind        ~> foo.induct
  foo.finite_ind ~> foo.finite_induct
  foo.coind      ~> foo.coinduct
  foo.casedist   ~> foo.exhaust
  foo.exhaust    ~> foo.nchotomy

* For consistency with other definition packages, the fixrec package
now generates qualified theorem names, INCOMPATIBILITY.

  foo_simps  ~> foo.simps
  foo_unfold ~> foo.unfold
  foo_induct ~> foo.induct

* The "fixrec_simp" attribute has been removed.  The "fixrec_simp"
method and internal fixrec proofs now use the default simpset instead.
INCOMPATIBILITY.

* The "contlub" predicate has been removed.  Proof scripts should use
lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.

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

* The constants cpair, cfst, and csnd have been removed in favor of
Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY.


*** ML ***

* Antiquotations for basic formal entities:

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

    @{type_name NAME}     -- logical type
    @{type_abbrev NAME}   -- type abbreviation
    @{nonterminal NAME}   -- type of concrete syntactic category
    @{type_syntax NAME}   -- syntax representation of any of the above

    @{const_name NAME}    -- logical constant (INCOMPATIBILITY)
    @{const_abbrev NAME}  -- abbreviated constant
    @{const_syntax NAME}  -- syntax representation of any of the above

* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
syntax constant (cf. 'syntax' command).

* Antiquotation @{make_string} inlines a function to print arbitrary
values similar to the ML toplevel.  The result is compiler dependent
and may fall back on "?" in certain situations.

* Diagnostic commands 'ML_val' and 'ML_command' may refer to
antiquotations @{Isar.state} and @{Isar.goal}.  This replaces impure
Isar.state() and Isar.goal(), which belong to the old TTY loop and do
not work with the asynchronous Isar document model.

* Configuration options now admit dynamic default values, depending on
the context or even global references.

* SHA1.digest digests strings according to SHA-1 (see RFC 3174).  It
uses an efficient external library if available (for Poly/ML).

* Renamed some important ML structures, while keeping the old names
for some time as aliases within the structure Legacy:

  OuterKeyword  ~>  Keyword
  OuterLex      ~>  Token
  OuterParse    ~>  Parse
  OuterSyntax   ~>  Outer_Syntax
  PrintMode     ~>  Print_Mode
  SpecParse     ~>  Parse_Spec
  ThyInfo       ~>  Thy_Info
  ThyLoad       ~>  Thy_Load
  ThyOutput     ~>  Thy_Output
  TypeInfer     ~>  Type_Infer

Note that "open Legacy" simplifies porting of sources, but forgetting
to remove it again will complicate porting again in the future.

* Most operations that refer to a global context are named
accordingly, e.g. Simplifier.global_context or
ProofContext.init_global.  There are some situations where a global
context actually works, but under normal circumstances one needs to
pass the proper local context through the code!

* Discontinued old TheoryDataFun with its copy/init operation -- data
needs to be pure.  Functor Theory_Data_PP retains the traditional
Pretty.pp argument to merge, which is absent in the standard
Theory_Data version.

* Sorts.certify_sort and derived "cert" operations for types and terms
no longer minimize sorts.  Thus certification at the boundary of the
inference kernel becomes invariant under addition of class relations,
which is an important monotonicity principle.  Sorts are now minimized
in the syntax layer only, at the boundary between the end-user and the
system.  Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
explicitly in rare situations.

* Renamed old-style Drule.standard to Drule.export_without_context, to
emphasize that this is in no way a standard operation.
INCOMPATIBILITY.

* Subgoal.FOCUS (and variants): resulting goal state is normalized as
usual for resolution.  Rare INCOMPATIBILITY.

* Renamed varify/unvarify operations to varify_global/unvarify_global
to emphasize that these only work in a global situation (which is
quite rare).

* Curried take and drop in library.ML; negative length is interpreted
as infinity (as in chop).  Subtle INCOMPATIBILITY.

* Proof terms: type substitutions on proof constants now use canonical
order of type variables.  INCOMPATIBILITY for tools working with proof
terms.

* Raw axioms/defs may no longer carry sort constraints, and raw defs
may no longer carry premises.  User-level specifications are
transformed accordingly by Thm.add_axiom/add_def.


*** System ***

* Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;
ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions.  Note that
proof terms are enabled unconditionally in the new HOL-Proofs image.

* Discontinued old ISABELLE and ISATOOL environment settings (legacy
feature since Isabelle2009).  Use ISABELLE_PROCESS and ISABELLE_TOOL,
respectively.

* Old lib/scripts/polyml-platform is superseded by the
ISABELLE_PLATFORM setting variable, which defaults to the 32 bit
variant, even on a 64 bit machine.  The following example setting
prefers 64 bit if available:

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

* The preliminary Isabelle/jEdit application demonstrates the emerging
Isabelle/Scala layer for advanced prover interaction and integration.
See src/Tools/jEdit or "isabelle jedit" provided by the properly built
component.



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.