NEWS

more correct NEWS;

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

New in this Isabelle version
----------------------------

*** General ***

* Significantly improved Isabelle/Isar implementation manual.

* Source files are always encoded as UTF-8, instead of old-fashioned
ISO-Latin-1.  INCOMPATIBILITY.  Isabelle LaTeX documents might require
the following package declarations:

  \usepackage[utf8]{inputenc}
  \usepackage{textcomp}

* Explicit treatment of UTF8 sequences as Isabelle symbols, such that
a Unicode character is treated as a single symbol, not a sequence of
non-ASCII bytes as before.  Since Isabelle/ML string literals may
contain symbols without further backslash escapes, Unicode can now be
used here as well.  Recall that Symbol.explode in ML provides a
consistent view on symbols, while raw explode (or String.explode)
merely give a byte-oriented representation.

* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
while the default heap location within that directory lacks that extra
suffix.  This isolates multiple Isabelle installations from each
other, avoiding problems with old settings in new versions.
INCOMPATIBILITY, need to copy/upgrade old user settings manually.

* Theory loading: only the master source file is looked-up in the
implicit load path, all other files are addressed relatively to its
directory.  Minor INCOMPATIBILITY, subtle change in semantics.

* Special treatment of ML file names has been discontinued.
Historically, optional extensions .ML or .sml were added on demand --
at the cost of clarity of file dependencies.  Recall that Isabelle/ML
files exclusively use the .ML extension.  Minor INCOMPATIBILTY.

* Various options that affect pretty printing etc. are now properly
handled within the context via configuration options, instead of
unsynchronized references or print modes.  There are both ML Config.T
entities and Isar declaration attributes to access these.

  ML (Config.T)                 Isar (attribute)

  eta_contract                  eta_contract
  show_brackets                 show_brackets
  show_sorts                    show_sorts
  show_types                    show_types
  show_question_marks           show_question_marks
  show_consts                   show_consts
  show_abbrevs                  show_abbrevs

  Syntax.ambiguity_level        syntax_ambiguity_level

  Goal_Display.goals_limit      goals_limit
  Goal_Display.show_main_goal   show_main_goal

  Thy_Output.display            thy_output_display
  Thy_Output.quotes             thy_output_quotes
  Thy_Output.indent             thy_output_indent
  Thy_Output.source             thy_output_source
  Thy_Output.break              thy_output_break

Note that corresponding "..._default" references in ML may be only
changed globally at the ROOT session setup, but *not* within a theory.
The option "show_abbrevs" supersedes the former print mode
"no_abbrevs" with inverted meaning.

* More systematic naming of some configuration options.
INCOMPATIBILTY.

  trace_simp  ~>  simp_trace
  debug_simp  ~>  simp_debug

* Support for real valued configuration options, using simplistic
floating-point notation that coincides with the inner syntax for
float_token.


*** Pure ***

* Command 'notepad' replaces former 'example_proof' for
experimentation in Isar without any result.  INCOMPATIBILITY.

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

* Interpretation command 'interpret' accepts a list of equations like
'interpretation' does.

* Diagnostic command 'print_interps' prints interpretations in proofs
in addition to interpretations in theories.

* Discontinued obsolete 'global' and 'local' commands to manipulate
the theory name space.  Rare INCOMPATIBILITY.  The ML functions
Sign.root_path and Sign.local_path may be applied directly where this
feature is still required for historical reasons.

* Discontinued obsolete 'constdefs' command.  INCOMPATIBILITY, use
'definition' instead.

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

* Document antiquotation @{file} checks file/directory entries within
the local file system.


*** HOL ***

* Quickcheck now by default uses exhaustive testing instead of random
testing.  Random testing can be invoked by quickcheck[random],
exhaustive testing by quickcheck[exhaustive].

* Quickcheck instantiates polymorphic types with small finite
datatypes by default. This enables a simple execution mechanism to
handle quantifiers and function equality over the finite datatypes.

* Functions can be declared as coercions and type inference will add
them as necessary upon input of a term. In theory Complex_Main,
real :: nat => real and real :: int => real are declared as
coercions. A new coercion function f is declared like this:

  declare [[coercion f]]

To lift coercions through type constructors (eg from nat => real to
nat list => real list), map functions can be declared, e.g.

  declare [[coercion_map map]]

Currently coercion inference is activated only in theories including
real numbers, i.e. descendants of Complex_Main.  This is controlled by
the configuration option "coercion_enabled", e.g. it can be enabled in
other theories like this:

  declare [[coercion_enabled]]

* Abandoned locales equiv, congruent and congruent2 for equivalence
relations.  INCOMPATIBILITY: use equivI rather than equiv_intro (same
for congruent(2)).

* Code generator: globbing constant expressions "*" and "Theory.*"
have been replaced by the more idiomatic "_" and "Theory._".
INCOMPATIBILITY.

* Theory Enum (for explicit enumerations of finite types) is now part
of the HOL-Main image. INCOMPATIBILITY: all constants of the Enum
theory now have to be referred to by its qualified name.

  enum    ~>  Enum.enum
  nlists  ~>  Enum.nlists
  product ~>  Enum.product

* Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
avoid confusion with finite sets.  INCOMPATIBILITY.

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

* Quickcheck now has a configurable time limit which is set to 30
seconds by default. This can be changed by adding [timeout = n] to the
quickcheck command. The time limit for Auto Quickcheck is still set
independently.

* Theory Multiset provides stable quicksort implementation of
sort_key.

* New command 'partial_function' provides basic support for recursive
function definitions over complete partial orders. Concrete instances
are provided for i) the option type, ii) tail recursion on arbitrary
types, and iii) the heap monad of Imperative_HOL. See
HOL/ex/Fundefs.thy and HOL/Imperative_HOL/ex/Linked_Lists.thy for
examples.

* Predicates "distinct" and "sorted" now defined inductively, with
nice induction rules.  INCOMPATIBILITY: former distinct.simps and
sorted.simps now named distinct_simps and sorted_simps.

* Constant "contents" renamed to "the_elem", to free the generic name
contents for other uses.  INCOMPATIBILITY.

* Dropped syntax for old primrec package.  INCOMPATIBILITY.

* Improved infrastructure for term evaluation using code generator
techniques, in particular static evaluation conversions.

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

* Renamed facts:
  expand_fun_eq  ~>  fun_eq_iff
  expand_set_eq  ~>  set_eq_iff
  set_ext        ~>  set_eqI
  nat_number     ~>  eval_nat_numeral

* Renamed class eq and constant eq (for code generation) to class
equal and constant equal, plus renaming of related facts and various
tuning.  INCOMPATIBILITY.

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

* Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.

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

* Theory SetsAndFunctions has been split into Function_Algebras and
Set_Algebras; canonical names for instance definitions for functions;
various improvements.  INCOMPATIBILITY.

* Records: logical foundation type for records do not carry a '_type'
suffix any longer.  INCOMPATIBILITY.

* Code generation for records: more idiomatic representation of record
types.  Warning: records are not covered by ancient SML code
generation any longer.  INCOMPATIBILITY.  In cases of need, a suitable
rep_datatype declaration helps to succeed then:

  record 'a foo = ...
  ...
  rep_datatype foo_ext ...

* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
INCOMPATIBILITY.

* Quickcheck in locales considers interpretations of that locale for
counter example search.

* Theory Library/Monad_Syntax provides do-syntax for monad types.
Syntax in Library/State_Monad has been changed to avoid ambiguities.
INCOMPATIBILITY.

* Code generator: export_code without explicit file declaration prints
to standard output.  INCOMPATIBILITY.

* Abolished some non-alphabetic type names: "prod" and "sum" replace
"*" and "+" respectively.  INCOMPATIBILITY.

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

* Constant "split" has been merged with constant "prod_case"; names of
ML functions, facts etc. involving split have been retained so far,
though.  INCOMPATIBILITY.

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

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

  constants
    null ~> List.null

  facts
    mem_iff ~> member_def
    null_empty ~> null_def

INCOMPATIBILITY.  Note that these were not suppossed to be used
regularly unless for striking reasons; their main purpose was code
generation.

* Some previously unqualified names have been qualified:

  types
    bool ~> HOL.bool
    nat ~> Nat.nat

  constants
    Trueprop ~> HOL.Trueprop
    True ~> HOL.True
    False ~> HOL.False
    op & ~> HOL.conj
    op | ~> HOL.disj
    op --> ~> HOL.implies
    op = ~> HOL.eq
    Not ~> HOL.Not
    The ~> HOL.The
    All ~> HOL.All
    Ex ~> HOL.Ex
    Ex1 ~> HOL.Ex1
    Let ~> HOL.Let
    If ~> HOL.If
    Ball ~> Set.Ball
    Bex ~> Set.Bex
    Suc ~> Nat.Suc
    Pair ~> Product_Type.Pair
    fst ~> Product_Type.fst
    snd ~> Product_Type.snd
    curry ~> Product_Type.curry
    op : ~> Set.member
    Collect ~> Set.Collect

INCOMPATIBILITY.

* Removed simplifier congruence rule of "prod_case", as has for long
been the case with "split".  INCOMPATIBILITY.

* Datatype package: theorems generated for executable equality (class
eq) carry proper names and are treated as default code equations.

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

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

* Multiset.thy: renamed empty_idemp -> empty_neutral

* code_simp.ML and method code_simp: simplification with rules
determined by code generator.

* code generator: do not print function definitions for case
combinators any longer.

* Multivariate Analysis: Introduced a type class for euclidean
space. Most theorems are now stated in terms of euclidean spaces
instead of finite cartesian products.

  types
    real ^ 'n ~>  'a::real_vector
              ~>  'a::euclidean_space
              ~>  'a::ordered_euclidean_space
        (depends on your needs)

  constants
     _ $ _        ~> _ $$ _
     \<chi> x. _  ~> \<chi>\<chi> x. _
     CARD('n)     ~> DIM('a)

Also note that the indices are now natural numbers and not from some
finite type. Finite cartesian products of euclidean spaces, products
of euclidean spaces the real and complex numbers are instantiated to
be euclidean_spaces.  INCOMPATIBILITY.

* Probability: Introduced pinfreal as real numbers with infinity. Use
pinfreal as value for measures. Introduce the Radon-Nikodym
derivative, product spaces and Fubini's theorem for arbitrary sigma
finite measures. Introduces Lebesgue measure based on the integral in
Multivariate Analysis.  INCOMPATIBILITY.

* Inductive package: offers new command 'inductive_simps' to
automatically derive instantiated and simplified equations for
inductive predicates, similar to 'inductive_cases'.

* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f"
is now an abbreviation of "range f = UNIV". The theorems bij_def and
surj_def are unchanged.  INCOMPATIBILITY.

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

* Weaker versions of the "meson" and "metis" proof methods are now
available in "HOL-Plain", without dependency on "Hilbert_Choice". The
proof methods become more powerful after "Hilbert_Choice" is loaded in
"HOL-Main".

* MESON: Renamed lemmas:
  meson_not_conjD ~> Meson.not_conjD
  meson_not_disjD ~> Meson.not_disjD
  meson_not_notD ~> Meson.not_notD
  meson_not_allD ~> Meson.not_allD
  meson_not_exD ~> Meson.not_exD
  meson_imp_to_disjD ~> Meson.imp_to_disjD
  meson_not_impD ~> Meson.not_impD
  meson_iff_to_disjD ~> Meson.iff_to_disjD
  meson_not_iffD ~> Meson.not_iffD
  meson_not_refl_disj_D ~> Meson.not_refl_disj_D
  meson_conj_exD1 ~> Meson.conj_exD1
  meson_conj_exD2 ~> Meson.conj_exD2
  meson_disj_exD ~> Meson.disj_exD
  meson_disj_exD1 ~> Meson.disj_exD1
  meson_disj_exD2 ~> Meson.disj_exD2
  meson_disj_assoc ~> Meson.disj_assoc
  meson_disj_comm ~> Meson.disj_comm
  meson_disj_FalseD1 ~> Meson.disj_FalseD1
  meson_disj_FalseD2 ~> Meson.disj_FalseD2
INCOMPATIBILITY.

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

* Sledgehammer:
  - Added "smt" and "remote_smt" provers based on the "smt" proof method. See
    the Sledgehammer manual for details ("isabelle doc sledgehammer").
  - Renamed lemmas:
    COMBI_def ~> Meson.COMBI_def
    COMBK_def ~> Meson.COMBK_def
    COMBB_def ~> Meson.COMBB_def
    COMBC_def ~> Meson.COMBC_def
    COMBS_def ~> Meson.COMBS_def
    abs_I ~> Meson.abs_I
    abs_K ~> Meson.abs_K
    abs_B ~> Meson.abs_B
    abs_C ~> Meson.abs_C
    abs_S ~> Meson.abs_S
    INCOMPATIBILITY.
  - Renamed commands:
    sledgehammer atp_info ~> sledgehammer running_provers
    sledgehammer atp_kill ~> sledgehammer kill_provers
    sledgehammer available_atps ~> sledgehammer available_provers
    INCOMPATIBILITY.
  - Renamed options:
    sledgehammer [atps = ...] ~> sledgehammer [provers = ...]
    sledgehammer [atp = ...] ~> sledgehammer [prover = ...]
    sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77]
    (and "ms" and "min" are no longer supported)
    INCOMPATIBILITY.

* Metis and Meson now have configuration options "meson_trace",
"metis_trace", and "metis_verbose" that can be enabled to diagnose
these tools. E.g.

    using [[metis_trace = true]]

* Nitpick:
  - Renamed options:
    nitpick [timeout = 77 s] ~> nitpick [timeout = 77]
    nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]
    INCOMPATIBILITY.
  - Now requires Kodkodi 1.2.9. INCOMPATIBILITY.
  - Added support for partial quotient types.
  - Added local versions of the "Nitpick.register_xxx" functions.
  - Added "whack" option.
  - Allow registration of quotient types as codatatypes.
  - Improved "merge_type_vars" option to merge more types.
  - Removed unsound "fast_descrs" option.
  - Added custom symmetry breaking for datatypes, making it possible to reach
    higher cardinalities.
  - Prevent the expansion of too large definitions.

* Changed SMT configuration options:
  - Renamed:
    z3_proofs ~> smt_oracle (with swapped semantics)
    z3_trace_assms ~> smt_trace_used_facts
    INCOMPATIBILITY.
  - Added:
    smt_verbose
    smt_datatypes
    cvc3_options
    yices_options

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

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


*** HOLCF ***

* The domain package now runs in definitional mode by default: The
former command 'new_domain' is now called 'domain'. To use the domain
package in its original axiomatic mode, use 'domain (unsafe)'.
INCOMPATIBILITY.

* The new class 'domain' is now the default sort; the definitional
domain package and the powerdomain theories both require this class.
The new class 'predomain' is an unpointed version of 'domain'.
Theories can be updated by replacing sort annotations as shown below.
INCOMPATIBILITY.

  'a::type ~> 'a::countable
  'a::cpo  ~> 'a::predomain
  'a::pcpo ~> 'a::domain

* The old type class 'rep' has been superseded by class 'domain'.
Accordingly, users of the definitional package must remove any
'default_sort rep' declarations. INCOMPATIBILITY.

* The old type classes 'profinite' and 'bifinite', along with the
overloaded constant 'approx' have been removed. INCOMPATIBILITY.

* The type 'udom alg_defl' has been replaced by the non-parameterized
type 'defl'. HOLCF no longer defines an embedding of type defl into
udom by default; the instance proof defl :: domain is now available in
HOLCF/Library/Defl_Bifinite.thy.

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

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

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

* Renamed some theorems (the original names are also still available).
  expand_fun_below   ~> fun_below_iff
  below_fun_ext      ~> fun_belowI
  expand_cfun_eq     ~> cfun_eq_iff
  ext_cfun           ~> cfun_eqI
  expand_cfun_below  ~> cfun_below_iff
  below_cfun_ext     ~> cfun_belowI
  cont2cont_Rep_CFun ~> cont2cont_APP

* The Abs and Rep functions for various types have changed names.
Related theorem names have also changed to match. INCOMPATIBILITY.
  Rep_CFun  ~> Rep_cfun
  Abs_CFun  ~> Abs_cfun
  Rep_Sprod ~> Rep_sprod
  Abs_Sprod ~> Abs_sprod
  Rep_Ssum  ~> Rep_ssum
  Abs_Ssum  ~> Abs_ssum

* Lemmas with names of the form *_defined_iff or *_strict_iff have
been renamed to *_bottom_iff. INCOMPATIBILITY.

* Various changes to bisimulation/coinduction with domain package:
  - Definitions of 'bisim' constants no longer mention definedness.
  - With mutual recursion, 'bisim' predicate is now curried.
  - With mutual recursion, each type gets a separate coind theorem.
  - Variable names in bisim_def and coinduct rules have changed.
INCOMPATIBILITY.

* Case combinators generated by the domain package for type 'foo' are
now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.

* Several theorems have been renamed to more accurately reflect the
names of constants and types involved. INCOMPATIBILITY.
  thelub_const    ~> lub_const
  lub_const       ~> is_lub_const
  thelubI         ~> lub_eqI
  is_lub_lub      ~> is_lubD2
  lubI            ~> is_lub_lub
  unique_lub      ~> is_lub_unique
  is_ub_lub       ~> is_lub_rangeD1
  lub_bin_chain   ~> is_lub_bin_chain
  thelub_Pair     ~> lub_Pair
  lub_cprod       ~> is_lub_prod
  thelub_cprod    ~> lub_prod
  minimal_cprod   ~> minimal_prod
  inst_cprod_pcpo ~> inst_prod_pcpo

* Many legacy theorem names have been discontinued. INCOMPATIBILITY.
  sq_ord_less_eq_trans ~> below_eq_trans
  sq_ord_eq_less_trans ~> eq_below_trans
  refl_less            ~> below_refl
  trans_less           ~> below_trans
  antisym_less         ~> below_antisym
  antisym_less_inverse ~> po_eq_conv [THEN iffD1]
  box_less             ~> box_below
  rev_trans_less       ~> rev_below_trans
  not_less2not_eq      ~> not_below2not_eq
  less_UU_iff          ~> below_UU_iff
  flat_less_iff        ~> flat_below_iff
  adm_less             ~> adm_below
  adm_not_less         ~> adm_not_below
  adm_compact_not_less ~> adm_compact_not_below
  less_fun_def         ~> below_fun_def
  expand_fun_less      ~> fun_below_iff
  less_fun_ext         ~> fun_belowI
  less_discr_def       ~> below_discr_def
  discr_less_eq        ~> discr_below_eq
  less_unit_def        ~> below_unit_def
  less_cprod_def       ~> below_prod_def
  prod_lessI           ~> prod_belowI
  Pair_less_iff        ~> Pair_below_iff
  fst_less_iff         ~> fst_below_iff
  snd_less_iff         ~> snd_below_iff
  expand_cfun_less     ~> cfun_below_iff
  less_cfun_ext        ~> cfun_belowI
  injection_less       ~> injection_below
  less_up_def          ~> below_up_def
  not_Iup_less         ~> not_Iup_below
  Iup_less             ~> Iup_below
  up_less              ~> up_below
  Def_inject_less_eq   ~> Def_below_Def
  Def_less_is_eq       ~> Def_below_iff
  spair_less_iff       ~> spair_below_iff
  less_sprod           ~> below_sprod
  spair_less           ~> spair_below
  sfst_less_iff        ~> sfst_below_iff
  ssnd_less_iff        ~> ssnd_below_iff
  fix_least_less       ~> fix_least_below
  dist_less_one        ~> dist_below_one
  less_ONE             ~> below_ONE
  ONE_less_iff         ~> ONE_below_iff
  less_sinlD           ~> below_sinlD
  less_sinrD           ~> below_sinrD


*** FOL and ZF ***

* All constant names are now qualified.  INCOMPATIBILITY.


*** ML ***

* Syntax.pretty_priority (default 0) configures the required priority
of pretty-printed output and thus affects insertion of parentheses.

* Syntax.default_root (default "any") configures the inner syntax
category (nonterminal symbol) for parsing of terms.

* Former exception Library.UnequalLengths now coincides with
ListPair.UnequalLengths.

* Renamed raw "explode" function to "raw_explode" to emphasize its
meaning.  Note that internally to Isabelle, Symbol.explode is used in
almost all situations.

* Discontinued obsolete function sys_error and exception SYS_ERROR.
See implementation manual for further details on exceptions in
Isabelle/ML.

* Antiquotation @{assert} inlines a function bool -> unit that raises
Fail if the argument is false.  Due to inlining the source position of
failed assertions is included in the error output.

* Discontinued antiquotation @{theory_ref}, which is obsolete since ML
text is in practice always evaluated with a stable theory checkpoint.
Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.

* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
meaning.

* Renamed structure PureThy to Pure_Thy and moved most of its
operations to structure Global_Theory, to emphasize that this is
rarely-used global-only stuff.

* Discontinued Output.debug.  Minor INCOMPATIBILITY, use plain writeln
instead (or tracing for high-volume output).

* Configuration option show_question_marks only affects regular pretty
printing of types and terms, not raw Term.string_of_vname.

* ML_Context.thm and ML_Context.thms are no longer pervasive.  Rare
INCOMPATIBILITY, superseded by static antiquotations @{thm} and
@{thms} for most purposes.

* ML structure Unsynchronized never opened, not even in Isar
interaction mode as before.  Old Unsynchronized.set etc. have been
discontinued -- use plain := instead.  This should be *rare* anyway,
since modern tools always work via official context data, notably
configuration options.

* ML antiquotations @{theory} and @{theory_ref} refer to named
theories from the ancestry of the current context, not any accidental
theory loader state as before.  Potential INCOMPATIBILITY, subtle
change in semantics.

* Parallel and asynchronous execution requires special care concerning
interrupts.  Structure Exn provides some convenience functions that
avoid working directly with raw Interrupt.  User code must not absorb
interrupts -- intermediate handling (for cleanup etc.) needs to be
followed by re-raising of the original exception.  Another common
source of mistakes are "handle _" patterns, which make the meaning of
the program subject to physical effects of the environment.


*** System ***

* The IsabelleText font now includes Cyrillic, Hebrew, Arabic from
DajaVu Sans.

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



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

*** General ***

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  using [[trace_simp = true]]

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

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

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


*** Pure ***

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

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

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

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

* Vacuous class specifications observe default sort.  INCOMPATIBILITY.

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

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

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

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

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

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

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

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

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


*** HOL ***

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

* New package for quotient types.  Commands 'quotient_type' and
'quotient_definition' may be used for defining types and constants by
quotient constructions.  An example is the type of integers created by
quotienting pairs of natural numbers:

  fun
    intrel :: "(nat * nat) => (nat * nat) => bool"
  where
    "intrel (x, y) (u, v) = (x + v = u + y)"

  quotient_type int = "nat * nat" / intrel
    by (auto simp add: equivp_def expand_fun_eq)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

* Real: new development using Cauchy Sequences.

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

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

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

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

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

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

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

    lower_semilattice                   ~> semilattice_inf
    upper_semilattice                   ~> semilattice_sup

    dense_linear_order                  ~> dense_linorder

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

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

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

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

INCOMPATIBILITY.

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

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

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

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

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

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

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

Renamed:

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

INCOMPATIBILITY.

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

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

* Theory List: added transpose.

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

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

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

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

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

* Method "induct" now takes instantiations of the form t, where t is not
  a variable, as a shorthand for "x == t", where x is a fresh variable.
  If this is not intended, t has to be enclosed in parentheses.
  By default, the equalities generated by definitional instantiations
  are pre-simplified, which may cause parameters of inductive cases
  to disappear, or may even delete some of the inductive cases.
  Use "induct (no_simp)" instead of "induct" to restore the old
  behaviour. The (no_simp) option is also understood by the "cases"
  and "nominal_induct" methods, which now perform pre-simplification, too.
  INCOMPATIBILITY.


*** HOLCF ***

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

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

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

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

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

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

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

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

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

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

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

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

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

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


*** ML ***

* Antiquotations for basic formal entities:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


*** System ***

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

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

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

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

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

* "IsabelleText" is a Unicode font derived from Bitstream Vera Mono
and Bluesky TeX fonts.  It provides the usual Isabelle symbols,
similar to the default assignment of the document preparation system
(cf. isabellesym.sty).  The Isabelle/Scala class Isabelle_System
provides some operations for direct access to the font without asking
the user for manual installation.



New in Isabelle2009-1 (December 2009)
-------------------------------------

*** General ***

* Discontinued old form of "escaped symbols" such as \\<forall>.  Only
one backslash should be used, even in ML sources.


*** Pure ***

* Locale interpretation propagates mixins along the locale hierarchy.
The currently only available mixins are the equations used to map
local definitions to terms of the target domain of an interpretation.

* Reactivated diagnostic command 'print_interps'.  Use "print_interps
loc" to print all interpretations of locale "loc" in the theory.
Interpretations in proofs are not shown.

* Thoroughly revised locales tutorial.  New section on conditional
interpretation.

* On instantiation of classes, remaining undefined class parameters
are formally declared.  INCOMPATIBILITY.


*** Document preparation ***

* New generalized style concept for printing terms: @{foo (style) ...}
instead of @{foo_style style ...}  (old form is still retained for
backward compatibility).  Styles can be also applied for
antiquotations prop, term_type and typeof.


*** HOL ***

* New proof method "smt" for a combination of first-order logic with
equality, linear and nonlinear (natural/integer/real) arithmetic, and
fixed-size bitvectors; there is also basic support for higher-order
features (esp. lambda abstractions).  It is an incomplete decision
procedure based on external SMT solvers using the oracle mechanism;
for the SMT solver Z3, this method is proof-producing.  Certificates
are provided to avoid calling the external solvers solely for
re-checking proofs.  Due to a remote SMT service there is no need for
installing SMT solvers locally.  See src/HOL/SMT.

* New commands to load and prove verification conditions generated by
the Boogie program verifier or derived systems (e.g. the Verifying C
Compiler (VCC) or Spec#).  See src/HOL/Boogie.

* New counterexample generator tool 'nitpick' based on the Kodkod
relational model finder.  See src/HOL/Tools/Nitpick and
src/HOL/Nitpick_Examples.

* New commands 'code_pred' and 'values' to invoke the predicate
compiler and to enumerate values of inductive predicates.

* A tabled implementation of the reflexive transitive closure.

* New implementation of quickcheck uses generic code generator;
default generators are provided for all suitable HOL types, records
and datatypes.  Old quickcheck can be re-activated importing theory
Library/SML_Quickcheck.

* New testing tool Mirabelle for automated proof tools.  Applies
several tools and tactics like sledgehammer, metis, or quickcheck, to
every proof step in a theory.  To be used in batch mode via the
"mirabelle" utility.

* New proof method "sos" (sum of squares) for nonlinear real
arithmetic (originally due to John Harison). It requires theory
Library/Sum_Of_Squares.  It is not a complete decision procedure but
works well in practice on quantifier-free real arithmetic with +, -,
*, ^, =, <= and <, i.e. boolean combinations of equalities and
inequalities between polynomials.  It makes use of external
semidefinite programming solvers.  Method "sos" generates a
certificate that can be pasted into the proof thus avoiding the need
to call an external tool every time the proof is checked.  See
src/HOL/Library/Sum_Of_Squares.

* New method "linarith" invokes existing linear arithmetic decision
procedure only.

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

* New Sledgehammer option "Full Types" in Proof General settings menu.
Causes full type information to be output to the ATPs.  This slows
ATPs down considerably but eliminates a source of unsound "proofs"
that fail later.