NEWS

fact consolidation

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

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

*** General ***

* Document antiquotation @{url} produces markup for the given URL,
which results in an active hyperlink within the text.

* Document antiquotation @{file_unchecked} is like @{file}, but does
not check existence within the file-system.

* Discontinued legacy_isub_isup, which was a temporary Isabelle/ML
workaround in Isabelle2013-1.  The prover process no longer accepts
old identifier syntax with \<^isub> or \<^isup>.

* Syntax of document antiquotation @{rail} now uses \<newline> instead
of "\\", to avoid the optical illusion of escaped backslash within
string token.  Minor INCOMPATIBILITY.

* Lexical syntax (inner and outer) supports text cartouches with
arbitrary nesting, and without escapes of quotes etc.  The Prover IDE
supports input via ` (backquote).

* The outer syntax categories "text" (for formal comments and document
markup commands) and "altstring" (for literal fact references) allow
cartouches as well, in addition to the traditional mix of quotations.

* More static checking of proof methods, which allows the system to
form a closure over the concrete syntax.  Method arguments should be
processed in the original proof context as far as possible, before
operating on the goal state.  In any case, the standard discipline for
subgoal-addressing needs to be observed: no subgoals or a subgoal
number that is out of range produces an empty result sequence, not an
exception.  Potential INCOMPATIBILITY for non-conformant tactical
proof tools.

* Support for official Standard ML within the Isabelle context.
Command 'SML_file' reads and evaluates the given Standard ML file.
Toplevel bindings are stored within the theory context; the initial
environment is restricted to the Standard ML implementation of
Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
and 'SML_export' allow to exchange toplevel bindings between the two
separate environments.  See also ~~/src/Tools/SML/Examples.thy for
some examples.


*** Prover IDE -- Isabelle/Scala/jEdit ***

* Improved syntactic and semantic completion mechanism:

  - No completion for Isar keywords that have already been recognized
    by the prover, e.g. ":" within accepted Isar syntax looses its
    meaning as abbreviation for symbol "\<in>".

  - Completion context provides information about embedded languages
    of Isabelle: keywords are only completed for outer syntax, symbols
    or antiquotations for languages that support them.  E.g. no symbol
    completion for ML source, but within ML strings, comments,
    antiquotations.

  - Support for semantic completion based on failed name space lookup.
    The error produced by the prover contains information about
    alternative names that are accessible in a particular position.
    This may be used with explicit completion (C+b) or implicit
    completion after some delay.

  - Semantic completions may get extended by appending a suffix of
    underscores to an already recognized name, e.g. "foo_" to complete
    "foo" or "foobar" if these are known in the context.  The special
    identifier "__" serves as a wild-card in this respect: it
    completes to the full collection of names from the name space
    (truncated according to the system option "completion_limit").

  - Syntax completion of the editor and semantic completion of the
    prover are merged.  Since the latter requires a full round-trip of
    document update to arrive, the default for option
    jedit_completion_delay has been changed to 0.5s to improve the
    user experience.

  - Option jedit_completion_immediate may now get used with
    jedit_completion_delay > 0, to complete symbol abbreviations
    aggressively while benefiting from combined syntactic and semantic
    completion.

  - Support for simple completion templates (with single
    place-holder), e.g. "`" for text cartouche, or "@{" for
    antiquotation.

  - Support for path completion within the formal text, based on
    file-system content.

  - Improved treatment of completion vs. various forms of jEdit text
    selection (multiple selections, rectangular selections,
    rectangular selection as "tall caret").

  - More reliable treatment of GUI events vs. completion popups: avoid
    loosing keystrokes with slow / remote graphics displays.

* Integrated spell-checker for document text, comments etc. with
completion popup and context-menu.  See also "Plugin Options /
Isabelle / General / Spell Checker" for some system options.

* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
Open text buffers take precedence over copies within the file-system.

* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
auxiliary ML files.

* Document panel: simplied interaction where every single mouse click
(re)opens document via desktop environment or as jEdit buffer.

* More general "Query" panel supersedes "Find" panel, with GUI access
to commands 'find_theorems' and 'find_consts', as well as print
operations for the context.  Minor incompatibility in keyboard
shortcuts etc.: replace action isabelle-find by isabelle-query.

* Search field for all output panels ("Output", "Query", "Info" etc.)
to highlight text via regular expression.

* Option "jedit_print_mode" (see also "Plugin Options / Isabelle /
General") allows to specify additional print modes for the prover
process, without requiring old-fashioned command-line invocation of
"isabelle jedit -m MODE".

* New panel: Simplifier trace.  Provides an interactive view of the
simplification process, enabled by the newly-introduced
"simplifier_trace" declaration.

* Support for Navigator plugin (with toolbar buttons).

* More support for remote files (e.g. http) using standard Java
networking operations instead of jEdit virtual file-systems.

* Improved Console/Scala plugin: more uniform scala.Console output,
more robust treatment of threads and interrupts.

* Improved management of dockable windows: clarified keyboard focus
and window placement wrt. main editor view; optional menu item to
"Detach" a copy where this makes sense.


*** Pure ***

* Basic constants of Pure use more conventional names and are always
qualified.  Rare INCOMPATIBILITY, but with potentially serious
consequences, notably for tools in Isabelle/ML.  The following
renaming needs to be applied:

  ==             ~>  Pure.eq
  ==>            ~>  Pure.imp
  all            ~>  Pure.all
  TYPE           ~>  Pure.type
  dummy_pattern  ~>  Pure.dummy_pattern

Systematic porting works by using the following theory setup on a
*previous* Isabelle version to introduce the new name accesses for the
old constants:

setup {*
  fn thy => thy
    |> Sign.root_path
    |> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="
    |> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"
    |> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"
    |> Sign.restore_naming thy
*}

Thus ML antiquotations like @{const_name Pure.eq} may be used already.
Later the application is moved to the current Isabelle version, and
the auxiliary aliases are deleted.

* Low-level type-class commands 'classes', 'classrel', 'arities' have
been discontinued to avoid the danger of non-trivial axiomatization
that is not immediately visible.  INCOMPATIBILITY, use regular
'instance' with proof.  The required OFCLASS(...) theorem might be
postulated via 'axiomatization' beforehand, or the proof finished
trivially if the underlying class definition is made vacuous (without
any assumptions).  See also Isabelle/ML operations
Axclass.axiomatize_class, Axclass.axiomatize_classrel,
Axclass.axiomatize_arity.

* Attributes "where" and "of" allow an optional context of local
variables ('for' declaration): these variables become schematic in the
instantiated theorem.

* Obsolete attribute "standard" has been discontinued (legacy since
Isabelle2012).  Potential INCOMPATIBILITY, use explicit 'for' context
where instantiations with schematic variables are intended (for
declaration commands like 'lemmas' or attributes like "of").  The
following temporary definition may help to port old applications:

  attribute_setup standard =
    "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"

* More thorough check of proof context for goal statements and
attributed fact expressions (concerning background theory, declared
hyps).  Potential INCOMPATIBILITY, tools need to observe standard
context discipline.  See also Assumption.add_assumes and the more
primitive Thm.assume_hyps.

* Inner syntax token language allows regular quoted strings "..."
(only makes sense in practice, if outer syntax is delimited
differently).

* Command 'print_term_bindings' supersedes 'print_binds' for clarity,
but the latter is retained some time as Proof General legacy.


*** HOL ***

* Command and antiquotation ''value'' are hardcoded against nbe and
ML now.  Minor INCOMPATIBILITY.

* Separate command ''approximate'' for approximative computation
in Decision_Procs/Approximation.  Minor INCOMPATIBILITY.

* Adjustion of INF and SUP operations:
  * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
  * Consolidated theorem names containing INFI and SUPR: have INF
  and SUP instead uniformly.
  * More aggressive normalization of expressions involving INF and Inf
  or SUP and Sup.
  * INF_image and SUP_image do not unfold composition.
  * Dropped facts INF_comp, SUP_comp.
  * Default congruence rules strong_INF_cong and strong_SUP_cong,
  with simplifier implication in premises.  Generalize and replace
  former INT_cong, SUP_cong
INCOMPATIBILITY.

* Swapped orientation of facts image_comp and vimage_comp:
  image_compose ~> image_comp [symmetric]
  image_comp ~> image_comp [symmetric]
  vimage_compose ~> vimage_comp [symmetric]
  vimage_comp ~> vimage_comp [symmetric]
  INCOMPATIBILITY.

* Simplifier: Enhanced solver of preconditions of rewrite rules
  can now deal with conjunctions.
  For help with converting proofs, the old behaviour of the simplifier
  can be restored like this:  declare/using [[simp_legacy_precond]]
  This configuration option will disappear again in the future.

* HOL-Word:
  * Abandoned fact collection "word_arith_alts", which is a
  duplicate of "word_arith_wis".
  * Dropped first (duplicated) element in fact collections
  "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
  "uint_word_arith_bintrs".

* Code generator: enforce case of identifiers only for strict
target language requirements.  INCOMPATIBILITY.

* Code generator: explicit proof contexts in many ML interfaces.
INCOMPATIBILITY.

* Code generator: minimize exported identifiers by default.
Minor INCOMPATIBILITY.

* Code generation for SML and OCaml: dropped arcane "no_signatures" option.
Minor INCOMPATIBILITY.

* Simproc "finite_Collect" is no longer enabled by default, due to
spurious crashes and other surprises.  Potential INCOMPATIBILITY.

* Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
  The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
  "primcorec", and "primcorecursive" commands are now part of "Main".
  Theory renamings:
    FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
    Library/Wfrec.thy ~> Wfrec.thy
    Library/Zorn.thy ~> Zorn.thy
    Cardinals/Order_Relation.thy ~> Order_Relation.thy
    Library/Order_Union.thy ~> Cardinals/Order_Union.thy
    Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy
    Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy
    Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy
    Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy
    Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy
    BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy
    BNF/Basic_BNFs.thy ~> Basic_BNFs.thy
    BNF/BNF_Comp.thy ~> BNF_Comp.thy
    BNF/BNF_Def.thy ~> BNF_Def.thy
    BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy
    BNF/BNF_GFP.thy ~> BNF_GFP.thy
    BNF/BNF_LFP.thy ~> BNF_LFP.thy
    BNF/BNF_Util.thy ~> BNF_Util.thy
    BNF/Coinduction.thy ~> Coinduction.thy
    BNF/More_BNFs.thy ~> Library/More_BNFs.thy
    BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy
    BNF/Examples/* ~> BNF_Examples/*
  New theories:
    Wellorder_Extension.thy (split from Zorn.thy)
    Library/Cardinal_Notations.thy
    Library/BNF_Axomatization.thy
    BNF_Examples/Misc_Primcorec.thy
    BNF_Examples/Stream_Processor.thy
  Discontinued theories:
    BNF/BNF.thy
    BNF/Equiv_Relations_More.thy
  INCOMPATIBILITY.

* New (co)datatype package:
  * "primcorec" is fully implemented.
  * "datatype_new" generates size functions ("size_xxx" and "size") as
    required by "fun".
  * BNFs are integrated with the Lifting tool and new-style (co)datatypes
    with Transfer.
  * Renamed commands:
      datatype_new_compat ~> datatype_compat
      primrec_new ~> primrec
      wrap_free_constructors ~> free_constructors
    INCOMPATIBILITY.
  * The generated constants "xxx_case" and "xxx_rec" have been renamed
    "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
    INCOMPATIBILITY.
  * The constant "xxx_(un)fold" and related theorems are no longer generated.
    Use "xxx_(co)rec" or define "xxx_(un)fold" manually using "prim(co)rec".
    INCOMPATIBILITY.
  * No discriminators are generated for nullary constructors by default,
    eliminating the need for the odd "=:" syntax.
    INCOMPATIBILITY.
  * No discriminators or selectors are generated by default by
    "datatype_new", unless custom names are specified or the new
    "discs_sels" option is passed.
    INCOMPATIBILITY.

* Old datatype package:
  * The generated theorems "xxx.cases" and "xxx.recs" have been renamed
    "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> "sum.case").
    INCOMPATIBILITY.
  * The generated constants "xxx_case", "xxx_rec", and "xxx_size" have been
    renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., "prod_case" ~>
    "case_prod").
    INCOMPATIBILITY.

* The types "'a list" and "'a option", their set and map functions, their
  relators, and their selectors are now produced using the new BNF-based
  datatype package.
  Renamed constants:
    Option.set ~> set_option
    Option.map ~> map_option
    option_rel ~> rel_option
  Renamed theorems:
    set_def ~> set_rec[abs_def]
    map_def ~> map_rec[abs_def]
    Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
    option.recs ~> option.rec
    list_all2_def ~> list_all2_iff
    set.simps ~> set_simps (or the slightly different "list.set")
    map.simps ~> list.map
    hd.simps ~> list.sel(1)
    tl.simps ~> list.sel(2-3)
    the.simps ~> option.sel
  INCOMPATIBILITY.

* The following map functions and relators have been renamed:
    sum_map ~> map_sum
    map_pair ~> map_prod
    prod_rel ~> rel_prod
    sum_rel ~> rel_sum
    fun_rel ~> rel_fun
    set_rel ~> rel_set
    filter_rel ~> rel_filter
    fset_rel ~> rel_fset (in "Library/FSet.thy")
    cset_rel ~> rel_cset (in "Library/Countable_Set_Type.thy")
    vset ~> rel_vset (in "Library/Quotient_Set.thy")

* New theories:
    Cardinals/Ordinal_Arithmetic.thy
    Library/Tree

* Theory reorganizations:
  * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy

* Consolidated some facts about big group operators:

    setsum_0' ~> setsum.neutral
    setsum_0 ~> setsum.neutral_const
    setsum_addf ~> setsum.distrib
    setsum_cartesian_product ~> setsum.cartesian_product
    setsum_cases ~> setsum.If_cases
    setsum_commute ~> setsum.commute
    setsum_cong ~> setsum.cong
    setsum_delta ~> setsum.delta
    setsum_delta' ~> setsum.delta'
    setsum_diff1' ~> setsum.remove
    setsum_empty ~> setsum.empty
    setsum_infinite ~> setsum.infinite
    setsum_insert ~> setsum.insert
    setsum_inter_restrict'' ~> setsum.inter_filter
    setsum_mono_zero_cong_left ~> setsum.mono_neutral_cong_left
    setsum_mono_zero_cong_right ~> setsum.mono_neutral_cong_right
    setsum_mono_zero_left ~> setsum.mono_neutral_left
    setsum_mono_zero_right ~> setsum.mono_neutral_right
    setsum_reindex ~> setsum.reindex
    setsum_reindex_cong ~> setsum.reindex_cong
    setsum_reindex_nonzero ~> setsum.reindex_nontrivial
    setsum_restrict_set ~> setsum.inter_restrict
    setsum_Plus ~> setsum.Plus
    setsum_setsum_restrict ~> setsum.commute_restrict
    setsum_Sigma ~> setsum.Sigma
    setsum_subset_diff ~> setsum.subset_diff
    setsum_Un_disjoint ~> setsum.union_disjoint
    setsum_UN_disjoint ~> setsum.UNION_disjoint
    setsum_Un_Int ~> setsum.union_inter
    setsum_Union_disjoint ~> setsum.Union_disjoint
    setsum_UNION_zero ~> setsum.Union_comp
    setsum_Un_zero ~> setsum.union_inter_neutral
    strong_setprod_cong ~> setprod.strong_cong
    strong_setsum_cong ~> setsum.strong_cong
    setprod_1' ~> setprod.neutral
    setprod_1 ~> setprod.neutral_const
    setprod_cartesian_product ~> setprod.cartesian_product
    setprod_cong ~> setprod.cong
    setprod_delta ~> setprod.delta
    setprod_delta' ~> setprod.delta'
    setprod_empty ~> setprod.empty
    setprod_infinite ~> setprod.infinite
    setprod_insert ~> setprod.insert
    setprod_mono_one_cong_left ~> setprod.mono_neutral_cong_left
    setprod_mono_one_cong_right ~> setprod.mono_neutral_cong_right
    setprod_mono_one_left ~> setprod.mono_neutral_left
    setprod_mono_one_right ~> setprod.mono_neutral_right
    setprod_reindex ~> setprod.reindex
    setprod_reindex_cong ~> setprod.reindex_cong
    setprod_reindex_nonzero ~> setprod.reindex_nontrivial
    setprod_Sigma ~> setprod.Sigma
    setprod_subset_diff ~> setprod.subset_diff
    setprod_timesf ~> setprod.distrib
    setprod_Un2 ~> setprod.union_diff2
    setprod_Un_disjoint ~> setprod.union_disjoint
    setprod_UN_disjoint ~> setprod.UNION_disjoint
    setprod_Un_Int ~> setprod.union_inter
    setprod_Union_disjoint ~> setprod.Union_disjoint
    setprod_Un_one ~> setprod.union_inter_neutral

  Dropped setsum_cong2 (simple variant of setsum.cong).
  Dropped setsum_inter_restrict' (simple variant of setsum.inter_restrict)
  Dropped setsum_reindex_id, setprod_reindex_id
    (simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]).

  INCOMPATIBILITY.

* New internal SAT solver "cdclite" that produces models and proof traces.
  This solver replaces the internal SAT solvers "enumerate" and "dpll".
  Applications that explicitly used one of these two SAT solvers should
  use "cdclite" instead. In addition, "cdclite" is now the default SAT
  solver for the "sat" and "satx" proof methods and corresponding tactics;
  the old default can be restored using
  "declare [[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY.

* SMT module:
  * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
    and supports recent versions of Z3 (e.g., 4.3). The new proof method is
    called "smt2". CVC3 and CVC4 are also supported as oracles. Yices is no
    longer supported, because no version of the solver can handle both
    SMT-LIB 2 and quantifiers.

* Sledgehammer:
  - Z3 can now produce Isar proofs.
  - MaSh overhaul:
      - New SML-based learning engines eliminate the dependency on Python
        and increase performance and reliability.
      - MaSh and MeSh are now used by default together with the traditional
        MePo (Meng-Paulson) relevance filter. To disable MaSh, set the "MaSh"
        system option in Plugin Options / Isabelle / General to "none". Other
        allowed values include "sml" (for the default SML engine) and "py"
        (for the old Python engine).
  - New option:
      smt_proofs
  - Renamed options:
      isar_compress ~> compress
      isar_try0 ~> try0
    INCOMPATIBILITY.

* Metis:
  - Removed legacy proof method 'metisFT'. Use 'metis (full_types)' instead.
    INCOMPATIBILITY.

* Try0: Added 'algebra' and 'meson' to the set of proof methods.

* Command renaming: enriched_type ~> functor. INCOMPATIBILITY.

* The symbol "\<newline>" may be used within char or string literals
to represent (Char Nibble0 NibbleA), i.e. ASCII newline.

* Activation of Z3 now works via "z3_non_commercial" system option
(without requiring restart), instead of former settings variable
"Z3_NON_COMMERCIAL".  The option can be edited in Isabelle/jEdit menu
Plugin Options / Isabelle / General.

* "declare [[code abort: ...]]" replaces "code_abort ...".
INCOMPATIBILITY.

* "declare [[code drop: ...]]" drops all code equations associated
with the given constants.

* Abolished slightly odd global lattice interpretation for min/max.

Fact consolidations:
    min_max.inf_assoc ~> min.assoc
    min_max.inf_commute ~> min.commute
    min_max.inf_left_commute ~> min.left_commute
    min_max.inf_idem ~> min.idem
    min_max.inf_left_idem ~> min.left_idem
    min_max.inf_right_idem ~> min.right_idem
    min_max.sup_assoc ~> max.assoc
    min_max.sup_commute ~> max.commute
    min_max.sup_left_commute ~> max.left_commute
    min_max.sup_idem ~> max.idem
    min_max.sup_left_idem ~> max.left_idem
    min_max.sup_inf_distrib1 ~> max_min_distrib2
    min_max.sup_inf_distrib2 ~> max_min_distrib1
    min_max.inf_sup_distrib1 ~> min_max_distrib2
    min_max.inf_sup_distrib2 ~> min_max_distrib1
    min_max.distrib ~> min_max_distribs
    min_max.inf_absorb1 ~> min.absorb1
    min_max.inf_absorb2 ~> min.absorb2
    min_max.sup_absorb1 ~> max.absorb1
    min_max.sup_absorb2 ~> max.absorb2
    min_max.le_iff_inf ~> min.absorb_iff1
    min_max.le_iff_sup ~> max.absorb_iff2
    min_max.inf_le1 ~> min.cobounded1
    min_max.inf_le2 ~> min.cobounded2
    le_maxI1, min_max.sup_ge1 ~> max.cobounded1
    le_maxI2, min_max.sup_ge2 ~> max.cobounded2
    min_max.le_infI1 ~> min.coboundedI1
    min_max.le_infI2 ~> min.coboundedI2
    min_max.le_supI1 ~> max.coboundedI1
    min_max.le_supI2 ~> max.coboundedI2
    min_max.less_infI1 ~> min.strict_coboundedI1
    min_max.less_infI2 ~> min.strict_coboundedI2
    min_max.less_supI1 ~> max.strict_coboundedI1
    min_max.less_supI2 ~> max.strict_coboundedI2
    min_max.inf_mono ~> min.mono
    min_max.sup_mono ~> max.mono
    min_max.le_infI, min_max.inf_greatest ~> min.boundedI
    min_max.le_supI, min_max.sup_least ~> max.boundedI
    min_max.le_inf_iff ~> min.bounded_iff
    min_max.le_sup_iff ~> max.bounded_iff

For min_max.inf_sup_aci, prefer (one of) min.commute, min.assoc,
min.left_commute, min.left_idem, max.commute, max.assoc,
max.left_commute, max.left_idem directly.

For min_max.inf_sup_ord, prefer (one of) min.cobounded1, min.cobounded2,
max.cobounded1m max.cobounded2 directly.

For min_ac or max_ac, prefer more general collection ac_simps.

INCOMPATBILITY.

* Word library: bit representations prefer type bool over type bit.
INCOMPATIBILITY.

* Theorem disambiguation Inf_le_Sup (on finite sets) ~> Inf_fin_le_Sup_fin.
INCOMPATIBILITY.

* Code generations are provided for make, fields, extend and truncate
operations on records.

* Qualified constant names Wellfounded.acc, Wellfounded.accp.
INCOMPATIBILITY.

* Fact generalization and consolidation:
    neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
INCOMPATIBILITY.

* Purely algebraic definition of even.  Fact generalization and consolidation:
    nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd
    even_zero_(nat|int) ~> even_zero
INCOMPATIBILITY.

* Abolished neg_numeral.
  * Canonical representation for minus one is "- 1".
  * Canonical representation for other negative numbers is "- (numeral _)".
  * When devising rule sets for number calculation, consider the
    following canonical cases: 0, 1, numeral _, - 1, - numeral _.
  * HOLogic.dest_number also recognizes numerals in non-canonical forms
    like "numeral One", "- numeral One", "- 0" and even "- ... - _".
  * Syntax for negative numerals is mere input syntax.
INCOMPATIBILITY.

* Elimination of fact duplicates:
    equals_zero_I ~> minus_unique
    diff_eq_0_iff_eq ~> right_minus_eq
    nat_infinite ~> infinite_UNIV_nat
    int_infinite ~> infinite_UNIV_int
INCOMPATIBILITY.

* Fact name consolidation:
    diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
    minus_le_self_iff ~> neg_less_eq_nonneg
    le_minus_self_iff ~> less_eq_neg_nonpos
    neg_less_nonneg ~> neg_less_pos
    less_minus_self_iff ~> less_neg_neg [simp]
INCOMPATIBILITY.

* More simplification rules on unary and binary minus:
add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,
add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
minus_add_cancel, uminus_add_conv_diff.  These correspondingly
have been taken away from fact collections algebra_simps and
field_simps.  INCOMPATIBILITY.

To restore proofs, the following patterns are helpful:

a) Arbitrary failing proof not involving "diff_def":
Consider simplification with algebra_simps or field_simps.

b) Lifting rules from addition to subtraction:
Try with "using <rule for addition> of [... "- _" ...]" by simp".

c) Simplification with "diff_def": just drop "diff_def".
Consider simplification with algebra_simps or field_simps;
or the brute way with
"simp add: diff_conv_add_uminus del: add_uminus_conv_diff".

* SUP and INF generalized to conditionally_complete_lattice

* Theory Lubs moved HOL image to HOL-Library. It is replaced by
Conditionally_Complete_Lattices.   INCOMPATIBILITY.

* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them
instead of explicitly stating boundedness of sets.

* ccpo.admissible quantifies only over non-empty chains to allow
more syntax-directed proof rules; the case of the empty chain
shows up as additional case in fixpoint induction proofs.
INCOMPATIBILITY

* Removed and renamed theorems in Series:
  summable_le         ~>  suminf_le
  suminf_le           ~>  suminf_le_const
  series_pos_le       ~>  setsum_le_suminf
  series_pos_less     ~>  setsum_less_suminf
  suminf_ge_zero      ~>  suminf_nonneg
  suminf_gt_zero      ~>  suminf_pos
  suminf_gt_zero_iff  ~>  suminf_pos_iff
  summable_sumr_LIMSEQ_suminf  ~>  summable_LIMSEQ
  suminf_0_le         ~>  suminf_nonneg [rotate]
  pos_summable        ~>  summableI_nonneg_bounded
  ratio_test          ~>  summable_ratio_test

  removed series_zero, replaced by sums_finite

  removed auxiliary lemmas:
    sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,
    half, le_Suc_ex_iff, lemma_realpow_diff_sumr, real_setsum_nat_ivl_bounded,
    summable_le2, ratio_test_lemma2, sumr_minus_one_realpow_zerom,
    sumr_one_lb_realpow_zero, summable_convergent_sumr_iff, sumr_diff_mult_const
INCOMPATIBILITY.

* Replace (F)DERIV syntax by has_derivative:
  - "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s : f'"

  - "(f has_field_derivative f') (at x within s)" replaces "DERIV f x : s : f'"

  - "f differentiable at x within s" replaces "_ differentiable _ in _" syntax

  - removed constant isDiff

  - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as input
    syntax.

  - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed

  - Renamed FDERIV_... lemmas to has_derivative_...

  - renamed deriv (the syntax constant used for "DERIV _ _ :> _") to DERIV

  - removed DERIV_intros, has_derivative_eq_intros

  - introduced derivative_intros and deriative_eq_intros which includes now rules for
    DERIV, has_derivative and has_vector_derivative.

  - Other renamings:
    differentiable_def        ~>  real_differentiable_def
    differentiableE           ~>  real_differentiableE
    fderiv_def                ~>  has_derivative_at
    field_fderiv_def          ~>  field_has_derivative_at
    isDiff_der                ~>  differentiable_def
    deriv_fderiv              ~>  has_field_derivative_def
    deriv_def                 ~>  DERIV_def
INCOMPATIBILITY.

* Include more theorems in continuous_intros. Remove the continuous_on_intros,
  isCont_intros collections, these facts are now in continuous_intros.

* Theorems about complex numbers are now stated only using Re and Im, the Complex
  constructor is not used anymore. It is possible to use primcorec to defined the
  behaviour of a complex-valued function.

  Removed theorems about the Complex constructor from the simpset, they are
  available as the lemma collection legacy_Complex_simps. This especially
  removes
    i_complex_of_real: "ii * complex_of_real r = Complex 0 r".

  Instead the reverse direction is supported with
    Complex_eq: "Complex a b = a + \<i> * b"

  Moved csqrt from Fundamental_Algebra_Theorem to Complex.

  Renamings:
    Re/Im                  ~>  complex.sel
    complex_Re/Im_zero     ~>  zero_complex.sel
    complex_Re/Im_add      ~>  plus_complex.sel
    complex_Re/Im_minus    ~>  uminus_complex.sel
    complex_Re/Im_diff     ~>  minus_complex.sel
    complex_Re/Im_one      ~>  one_complex.sel
    complex_Re/Im_mult     ~>  times_complex.sel
    complex_Re/Im_inverse  ~>  inverse_complex.sel
    complex_Re/Im_scaleR   ~>  scaleR_complex.sel
    complex_Re/Im_i        ~>  ii.sel
    complex_Re/Im_cnj      ~>  cnj.sel
    Re/Im_cis              ~>  cis.sel

    complex_divide_def   ~>  divide_complex_def
    complex_norm_def     ~>  norm_complex_def
    cmod_def             ~>  norm_complex_de

  Removed theorems:
    complex_zero_def
    complex_add_def
    complex_minus_def
    complex_diff_def
    complex_one_def
    complex_mult_def
    complex_inverse_def
    complex_scaleR_def

* Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.

* Nitpick:
  - Fixed soundness bug whereby mutually recursive datatypes could take
    infinite values.
  - Fixed soundness bug with low-level number functions such as "Abs_Integ" and
    "Rep_Integ".
  - Removed "std" option.
  - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
    "hide_types".

* HOL-Multivariate_Analysis:
  - type class ordered_real_vector for ordered vector spaces
  - new theory Complex_Basic_Analysis defining complex derivatives,
    holomorphic functions, etc., ported from HOL Light's canal.ml.
  - changed order of ordered_euclidean_space to be compatible with
    pointwise ordering on products. Therefore instance of
    conditionally_complete_lattice and ordered_real_vector.
    INCOMPATIBILITY: use box instead of greaterThanLessThan or
    explicit set-comprehensions with eucl_less for other (half-) open
    intervals.

  - renamed theorems:
    derivative_linear         ~>  has_derivative_bounded_linear
    derivative_is_linear      ~>  has_derivative_linear
    bounded_linear_imp_linear ~>  bounded_linear.linear

* HOL-Probability:
  - replaced the Lebesgue integral on real numbers by the more general Bochner
    integral for functions into a real-normed vector space.

    integral_zero               ~>  integral_zero / integrable_zero
    integral_minus              ~>  integral_minus / integrable_minus
    integral_add                ~>  integral_add / integrable_add
    integral_diff               ~>  integral_diff / integrable_diff
    integral_setsum             ~>  integral_setsum / integrable_setsum
    integral_multc              ~>  integral_mult_left / integrable_mult_left
    integral_cmult              ~>  integral_mult_right / integrable_mult_right
    integral_triangle_inequality~>  integral_norm_bound
    integrable_nonneg           ~>  integrableI_nonneg
    integral_positive           ~>  integral_nonneg_AE
    integrable_abs_iff          ~>  integrable_abs_cancel
    positive_integral_lim_INF   ~>  positive_integral_liminf
    lebesgue_real_affine        ~>  lborel_real_affine
    borel_integral_has_integral ~>  has_integral_lebesgue_integral
    integral_indicator          ~>
         integral_real_indicator / integrable_real_indicator
    positive_integral_fst       ~>  positive_integral_fst'
    positive_integral_fst_measurable ~> positive_integral_fst
    positive_integral_snd_measurable ~> positive_integral_snd

    integrable_fst_measurable   ~>
         integral_fst / integrable_fst / AE_integrable_fst

    integrable_snd_measurable   ~>
         integral_snd / integrable_snd / AE_integrable_snd

    integral_monotone_convergence  ~>
         integral_monotone_convergence / integrable_monotone_convergence

    integral_monotone_convergence_at_top  ~>
         integral_monotone_convergence_at_top /
         integrable_monotone_convergence_at_top

    has_integral_iff_positive_integral_lebesgue  ~>
         has_integral_iff_has_bochner_integral_lebesgue_nonneg

    lebesgue_integral_has_integral  ~>
         has_integral_integrable_lebesgue_nonneg

    positive_integral_lebesgue_has_integral  ~>
         integral_has_integral_lebesgue_nonneg /
         integrable_has_integral_lebesgue_nonneg

    lebesgue_integral_real_affine  ~>
         positive_integral_real_affine

    has_integral_iff_positive_integral_lborel  ~>
         integral_has_integral_nonneg / integrable_has_integral_nonneg

    The following theorems where removed:

    lebesgue_integral_nonneg
    lebesgue_integral_uminus
    lebesgue_integral_cmult
    lebesgue_integral_multc
    lebesgue_integral_cmult_nonneg
    integral_cmul_indicator
    integral_real

  - Renamed positive_integral to nn_integral:

    * Renamed all lemmas "*positive_integral*" to *nn_integral*"
      positive_integral_positive ~> nn_integral_nonneg

    * Renamed abbreviation integral\<^sup>P to integral\<^sup>N.

  - Formalized properties about exponentially, Erlang, and normal distributed
    random variables.

* Library/Kleene-Algebra was removed because AFP/Kleene_Algebra subsumes it.

*** Scala ***

* The signature and semantics of Document.Snapshot.cumulate_markup /
select_markup have been clarified.  Markup is now traversed in the
order of reports given by the prover: later markup is usually more
specific and may override results accumulated so far.  The elements
guard is mandatory and checked precisely.  Subtle INCOMPATIBILITY.


*** ML ***

* Moved ML_Compiler.exn_trace and other operations on exceptions to
structure Runtime.  Minor INCOMPATIBILITY.

* Discontinued old Toplevel.debug in favour of system option
"ML_exception_trace", which may be also declared within the context via
"declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.

* Renamed configuration option "ML_trace" to "ML_source_trace". Minor
INCOMPATIBILITY.

* Configuration option "ML_print_depth" controls the pretty-printing
depth of the ML compiler within the context.  The old print_depth in
ML is still available as default_print_depth, but rarely used.  Minor
INCOMPATIBILITY.

* Proper context discipline for read_instantiate and instantiate_tac:
variables that are meant to become schematic need to be given as
fixed, and are generalized by the explicit context of local variables.
This corresponds to Isar attributes "where" and "of" with 'for'
declaration.  INCOMPATIBILITY, also due to potential change of indices
of schematic variables.

* Toplevel function "use" refers to raw ML bootstrap environment,
without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
Note that 'ML_file' is the canonical command to load ML files into the
formal context.

* Proper context for basic Simplifier operations: rewrite_rule,
rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to
pass runtime Proof.context (and ensure that the simplified entity
actually belongs to it).

* Subtle change of semantics of Thm.eq_thm: theory stamps are not
compared (according to Thm.thm_ord), but assumed to be covered by the
current background theory.  Thus equivalent data produced in different
branches of the theory graph usually coincides (e.g. relevant for
theory merge).  Note that the softer Thm.eq_thm_prop is often more
appropriate than Thm.eq_thm.

* Simplified programming interface to define ML antiquotations, see
structure ML_Antiquotation.  Minor INCOMPATIBILITY.

* ML antiquotation @{here} refers to its source position, which is
occasionally useful for experimentation and diagnostic purposes.

* ML antiquotation @{path} produces a Path.T value, similarly to
Path.explode, but with compile-time check against the file-system and
some PIDE markup.  Note that unlike theory source, ML does not have a
well-defined master directory, so an absolute symbolic path
specification is usually required, e.g. "~~/src/HOL".

* ML antiquotation @{print} inlines a function to print an arbitrary
ML value, which is occasionally useful for diagnostic or demonstration
purposes.


*** System ***

* Session ROOT specifications require explicit 'document_files' for
robust dependencies on LaTeX sources.  Only these explicitly given
files are copied to the document output directory, before document
processing is started.

* Simplified "isabelle display" tool.  Settings variables DVI_VIEWER
and PDF_VIEWER now refer to the actual programs, not shell
command-lines.  Discontinued option -c: invocation may be asynchronous
via desktop environment, without any special precautions.  Potential
INCOMPATIBILITY with ambitious private settings.

* Improved 'display_drafts' concerning desktop integration and
repeated invocation in PIDE front-end: re-use single file
$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.

* The raw Isabelle process executable has been renamed from
"isabelle-process" to "isabelle_process", which conforms to common
shell naming conventions, and allows to define a shell function within
the Isabelle environment to avoid dynamic path lookup.  Rare
incompatibility for old tools that do not use the $ISABELLE_PROCESS
settings variable yet.

* Removed obsolete "isabelle unsymbolize".  Note that the usual format
for email communication is the Unicode rendering of Isabelle symbols,
as produced by Isabelle/jEdit, for example.

* Retired the now unused Isabelle tool "wwwfind". Similar
functionality may be integrated into PIDE/jEdit at a later point.

* Windows: support for regular TeX installation (e.g. MiKTeX) instead
of TeX Live from Cygwin.



New in Isabelle2013-2 (December 2013)
-------------------------------------

*** Prover IDE -- Isabelle/Scala/jEdit ***

* More robust editing of running commands with internal forks,
e.g. non-terminating 'by' steps.

* More relaxed Sledgehammer panel: avoid repeated application of query
after edits surrounding the command location.

* More status information about commands that are interrupted
accidentally (via physical event or Poly/ML runtime system signal,
e.g. out-of-memory).


*** System ***

* More robust termination of external processes managed by
Isabelle/ML: support cancellation of tasks within the range of
milliseconds, as required for PIDE document editing with automatically
tried tools (e.g. Sledgehammer).

* Reactivated Isabelle/Scala kill command for external processes on
Mac OS X, which was accidentally broken in Isabelle2013-1 due to a
workaround for some Debian/Ubuntu Linux versions from 2013.



New in Isabelle2013-1 (November 2013)
-------------------------------------

*** General ***

* Discontinued obsolete 'uses' within theory header.  Note that
commands like 'ML_file' work without separate declaration of file
dependencies.  Minor INCOMPATIBILITY.

* Discontinued redundant 'use' command, which was superseded by
'ML_file' in Isabelle2013.  Minor INCOMPATIBILITY.

* Simplified subscripts within identifiers, using plain \<^sub>
instead of the second copy \<^isub> and \<^isup>.  Superscripts are
only for literal tokens within notation; explicit mixfix annotations
for consts or fixed variables may be used as fall-back for unusual
names.  Obsolete \<twosuperior> has been expanded to \<^sup>2 in
Isabelle/HOL.  INCOMPATIBILITY, use "isabelle update_sub_sup" to
standardize symbols as a starting point for further manual cleanup.
The ML reference variable "legacy_isub_isup" may be set as temporary
workaround, to make the prover accept a subset of the old identifier
syntax.

* Document antiquotations: term style "isub" has been renamed to
"sub".  Minor INCOMPATIBILITY.

* Uniform management of "quick_and_dirty" as system option (see also
"isabelle options"), configuration option within the context (see also
Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor
INCOMPATIBILITY, need to use more official Isabelle means to access
quick_and_dirty, instead of historical poking into mutable reference.

* Renamed command 'print_configs' to 'print_options'.  Minor
INCOMPATIBILITY.

* Proper diagnostic command 'print_state'.  Old 'pr' (with its
implicit change of some global references) is retained for now as
control command, e.g. for ProofGeneral 3.7.x.

* Discontinued 'print_drafts' command with its old-fashioned PS output
and Unix command-line print spooling.  Minor INCOMPATIBILITY: use
'display_drafts' instead and print via the regular document viewer.

* Updated and extended "isar-ref" and "implementation" manual,
eliminated old "ref" manual.


*** Prover IDE -- Isabelle/Scala/jEdit ***

* New manual "jedit" for Isabelle/jEdit, see isabelle doc or
Documentation panel.

* Dockable window "Documentation" provides access to Isabelle
documentation.

* Dockable window "Find" provides query operations for formal entities
(GUI front-end to 'find_theorems' command).

* Dockable window "Sledgehammer" manages asynchronous / parallel
sledgehammer runs over existing document sources, independently of
normal editing and checking process.

* Dockable window "Timing" provides an overview of relevant command
timing information, depending on option jedit_timing_threshold.  The
same timing information is shown in the extended tooltip of the
command keyword, when hovering the mouse over it while the CONTROL or
COMMAND modifier is pressed.

* Improved dockable window "Theories": Continuous checking of proof
document (visible and required parts) may be controlled explicitly,
using check box or shortcut "C+e ENTER".  Individual theory nodes may
be marked explicitly as required and checked in full, using check box
or shortcut "C+e SPACE".

* Improved completion mechanism, which is now managed by the
Isabelle/jEdit plugin instead of SideKick.  Refined table of Isabelle
symbol abbreviations (see $ISABELLE_HOME/etc/symbols).

* Standard jEdit keyboard shortcut C+b complete-word is remapped to
isabelle.complete for explicit completion in Isabelle sources.
INCOMPATIBILITY wrt. jEdit defaults, may have to invent new shortcuts
to resolve conflict.

* Improved support of various "minor modes" for Isabelle NEWS,
options, session ROOT etc., with completion and SideKick tree view.

* Strictly monotonic document update, without premature cancellation of
running transactions that are still needed: avoid reset/restart of
such command executions while editing.

* Support for asynchronous print functions, as overlay to existing
document content.

* Support for automatic tools in HOL, which try to prove or disprove
toplevel theorem statements.

* Action isabelle.reset-font-size resets main text area font size
according to Isabelle/Scala plugin option "jedit_font_reset_size" (see
also "Plugin Options / Isabelle / General").  It can be bound to some
keyboard shortcut by the user (e.g. C+0 and/or C+NUMPAD0).

* File specifications in jEdit (e.g. file browser) may refer to
$ISABELLE_HOME and $ISABELLE_HOME_USER on all platforms.  Discontinued
obsolete $ISABELLE_HOME_WINDOWS variable.

* Improved support for Linux look-and-feel "GTK+", see also "Utilities
/ Global Options / Appearance".

* Improved support of native Mac OS X functionality via "MacOSX"
plugin, which is now enabled by default.


*** Pure ***

* Commands 'interpretation' and 'sublocale' are now target-sensitive.
In particular, 'interpretation' allows for non-persistent
interpretation within "context ... begin ... end" blocks offering a
light-weight alternative to 'sublocale'.  See "isar-ref" manual for
details.

* Improved locales diagnostic command 'print_dependencies'.

* Discontinued obsolete 'axioms' command, which has been marked as
legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'
instead, while observing its uniform scope for polymorphism.

* Discontinued empty name bindings in 'axiomatization'.
INCOMPATIBILITY.

* System option "proofs" has been discontinued.  Instead the global
state of Proofterm.proofs is persistently compiled into logic images
as required, notably HOL-Proofs.  Users no longer need to change
Proofterm.proofs dynamically.  Minor INCOMPATIBILITY.

* Syntax translation functions (print_translation etc.) always depend
on Proof.context.  Discontinued former "(advanced)" option -- this is
now the default.  Minor INCOMPATIBILITY.

* Former global reference trace_unify_fail is now available as
configuration option "unify_trace_failure" (global context only).

* SELECT_GOAL now retains the syntactic context of the overall goal
state (schematic variables etc.).  Potential INCOMPATIBILITY in rare
situations.


*** HOL ***

* Stronger precedence of syntax for big intersection and union on
sets, in accordance with corresponding lattice operations.
INCOMPATIBILITY.

* Notation "{p:A. P}" now allows tuple patterns as well.

* Nested case expressions are now translated in a separate check phase
rather than during parsing. The data for case combinators is separated
from the datatype package. The declaration attribute
"case_translation" can be used to register new case combinators:

  declare [[case_translation case_combinator constructor1 ... constructorN]]

* Code generator:
  - 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' /
    'code_instance'.
  - 'code_identifier' declares name hints for arbitrary identifiers in
    generated code, subsuming 'code_modulename'.

See the isar-ref manual for syntax diagrams, and the HOL theories for
examples.

* Attibute 'code': 'code' now declares concrete and abstract code
equations uniformly.  Use explicit 'code equation' and 'code abstract'
to distinguish both when desired.

* Discontinued theories Code_Integer and Efficient_Nat by a more
fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,
Code_Target_Nat and Code_Target_Numeral.  See the tutorial on code
generation for details.  INCOMPATIBILITY.

* Numeric types are mapped by default to target language numerals:
natural (replaces former code_numeral) and integer (replaces former
code_int).  Conversions are available as integer_of_natural /
natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and
Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in
ML).  INCOMPATIBILITY.

* Function package: For mutually recursive functions f and g, separate
cases rules f.cases and g.cases are generated instead of unusable
f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,
in the case that the unusable rule was used nevertheless.

* Function package: For each function f, new rules f.elims are
generated, which eliminate equalities of the form "f x = t".

* New command 'fun_cases' derives ad-hoc elimination rules for
function equations as simplified instances of f.elims, analogous to
inductive_cases.  See ~~/src/HOL/ex/Fundefs.thy for some examples.

* Lifting:
  - parametrized correspondence relations are now supported:
    + parametricity theorems for the raw term can be specified in
      the command lift_definition, which allow us to generate stronger
      transfer rules
    + setup_lifting generates stronger transfer rules if parametric
      correspondence relation can be generated
    + various new properties of the relator must be specified to support
      parametricity
    + parametricity theorem for the Quotient relation can be specified
  - setup_lifting generates domain rules for the Transfer package
  - stronger reflexivity prover of respectfulness theorems for type
    copies
  - ===> and --> are now local. The symbols can be introduced
    by interpreting the locale lifting_syntax (typically in an
    anonymous context)
  - Lifting/Transfer relevant parts of Library/Quotient_* are now in
    Main. Potential INCOMPATIBILITY
  - new commands for restoring and deleting Lifting/Transfer context:
    lifting_forget, lifting_update
  - the command print_quotmaps was renamed to print_quot_maps.
    INCOMPATIBILITY

* Transfer:
  - better support for domains in Transfer: replace Domainp T
    by the actual invariant in a transferred goal
  - transfer rules can have as assumptions other transfer rules
  - Experimental support for transferring from the raw level to the
    abstract level: Transfer.transferred attribute
  - Attribute version of the transfer method: untransferred attribute

* Reification and reflection:
  - Reification is now directly available in HOL-Main in structure
    "Reification".
  - Reflection now handles multiple lists with variables also.
  - The whole reflection stack has been decomposed into conversions.
INCOMPATIBILITY.

* Revised devices for recursive definitions over finite sets:
  - Only one fundamental fold combinator on finite set remains:
    Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b
    This is now identity on infinite sets.
  - Locales ("mini packages") for fundamental definitions with
    Finite_Set.fold: folding, folding_idem.
  - Locales comm_monoid_set, semilattice_order_set and
    semilattice_neutr_order_set for big operators on sets.
    See theory Big_Operators for canonical examples.
    Note that foundational constants comm_monoid_set.F and
    semilattice_set.F correspond to former combinators fold_image
    and fold1 respectively.  These are now gone.  You may use
    those foundational constants as substitutes, but it is
    preferable to interpret the above locales accordingly.
  - Dropped class ab_semigroup_idem_mult (special case of lattice,
    no longer needed in connection with Finite_Set.fold etc.)
  - Fact renames:
      card.union_inter ~> card_Un_Int [symmetric]
      card.union_disjoint ~> card_Un_disjoint
INCOMPATIBILITY.

* Locale hierarchy for abstract orderings and (semi)lattices.

* Complete_Partial_Order.admissible is defined outside the type class
ccpo, but with mandatory prefix ccpo. Admissibility theorems lose the
class predicate assumption or sort constraint when possible.
INCOMPATIBILITY.

* Introduce type class "conditionally_complete_lattice": Like a
complete lattice but does not assume the existence of the top and
bottom elements.  Allows to generalize some lemmas about reals and
extended reals.  Removed SupInf and replaced it by the instantiation
of conditionally_complete_lattice for real. Renamed lemmas about
conditionally-complete lattice from Sup_... to cSup_... and from
Inf_...  to cInf_... to avoid hidding of similar complete lattice
lemmas.

* Introduce type class linear_continuum as combination of
conditionally-complete lattices and inner dense linorders which have
more than one element.  INCOMPATIBILITY.

* Introduced type classes order_top and order_bot. The old classes top
and bot only contain the syntax without assumptions.  INCOMPATIBILITY:
Rename bot -> order_bot, top -> order_top

* Introduce type classes "no_top" and "no_bot" for orderings without
top and bottom elements.

* Split dense_linorder into inner_dense_order and no_top, no_bot.

* Complex_Main: Unify and move various concepts from
HOL-Multivariate_Analysis to HOL-Complex_Main.

 - Introduce type class (lin)order_topology and
   linear_continuum_topology.  Allows to generalize theorems about
   limits and order.  Instances are reals and extended reals.

 - continuous and continuos_on from Multivariate_Analysis:
   "continuous" is the continuity of a function at a filter.  "isCont"
   is now an abbrevitation: "isCont x f == continuous (at _) f".

   Generalized continuity lemmas from isCont to continuous on an
   arbitrary filter.

 - compact from Multivariate_Analysis. Use Bolzano's lemma to prove
   compactness of closed intervals on reals. Continuous functions
   attain infimum and supremum on compact sets. The inverse of a
   continuous function is continuous, when the function is continuous
   on a compact set.

 - connected from Multivariate_Analysis. Use it to prove the
   intermediate value theorem. Show connectedness of intervals on
   linear_continuum_topology).

 - first_countable_topology from Multivariate_Analysis. Is used to
   show equivalence of properties on the neighbourhood filter of x and
   on all sequences converging to x.

 - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved
   theorems from Library/FDERIV.thy to Deriv.thy and base the
   definition of DERIV on FDERIV. Add variants of DERIV and FDERIV
   which are restricted to sets, i.e. to represent derivatives from
   left or right.

 - Removed the within-filter. It is replaced by the principal filter:

     F within X = inf F (principal X)

 - Introduce "at x within U" as a single constant, "at x" is now an
   abbreviation for "at x within UNIV"

 - Introduce named theorem collections tendsto_intros,
   continuous_intros, continuous_on_intros and FDERIV_intros. Theorems
   in tendsto_intros (or FDERIV_intros) are also available as
   tendsto_eq_intros (or FDERIV_eq_intros) where the right-hand side
   is replaced by a congruence rule. This allows to apply them as
   intro rules and then proving equivalence by the simplifier.

 - Restructured theories in HOL-Complex_Main:

   + Moved RealDef and RComplete into Real

   + Introduced Topological_Spaces and moved theorems about
     topological spaces, filters, limits and continuity to it

   + Renamed RealVector to Real_Vector_Spaces

   + Split Lim, SEQ, Series into Topological_Spaces,
     Real_Vector_Spaces, and Limits

   + Moved Ln and Log to Transcendental

   + Moved theorems about continuity from Deriv to Topological_Spaces

 - Remove various auxiliary lemmas.

INCOMPATIBILITY.

* Nitpick:
  - Added option "spy".
  - Reduce incidence of "too high arity" errors.

* Sledgehammer:
  - Renamed option:
      isar_shrink ~> isar_compress
    INCOMPATIBILITY.
  - Added options "isar_try0", "spy".
  - Better support for "isar_proofs".
  - MaSh has been fined-tuned and now runs as a local server.

* Improved support for ad hoc overloading of constants (see also
isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).

* Library/Polynomial.thy:
  - Use lifting for primitive definitions.
  - Explicit conversions from and to lists of coefficients, used for
    generated code.
  - Replaced recursion operator poly_rec by fold_coeffs.
  - Prefer pre-existing gcd operation for gcd.
  - Fact renames:
    poly_eq_iff ~> poly_eq_poly_eq_iff
    poly_ext ~> poly_eqI
    expand_poly_eq ~> poly_eq_iff
IMCOMPATIBILITY.

* New Library/Simps_Case_Conv.thy: Provides commands simps_of_case and
case_of_simps to convert function definitions between a list of
equations with patterns on the lhs and a single equation with case
expressions on the rhs. See also Ex/Simps_Case_Conv_Examples.thy.

* New Library/FSet.thy: type of finite sets defined as a subtype of
sets defined by Lifting/Transfer.

* Discontinued theory src/HOL/Library/Eval_Witness.  INCOMPATIBILITY.

* Consolidation of library theories on product orders:

    Product_Lattice ~> Product_Order -- pointwise order on products
    Product_ord ~> Product_Lexorder -- lexicographic order on products

INCOMPATIBILITY.

* Imperative-HOL: The MREC combinator is considered legacy and no
longer included by default. INCOMPATIBILITY, use partial_function
instead, or import theory Legacy_Mrec as a fallback.

* HOL-Algebra: Discontinued theories ~~/src/HOL/Algebra/abstract and
~~/src/HOL/Algebra/poly.  Existing theories should be based on
~~/src/HOL/Library/Polynomial instead.  The latter provides
integration with HOL's type classes for rings.  INCOMPATIBILITY.

* HOL-BNF:
  - Various improvements to BNF-based (co)datatype package, including
    new commands "primrec_new", "primcorec", and
    "datatype_new_compat", as well as documentation. See
    "datatypes.pdf" for details.
  - New "coinduction" method to avoid some boilerplate (compared to
    coinduct).
  - Renamed keywords:
    data ~> datatype_new
    codata ~> codatatype
    bnf_def ~> bnf
  - Renamed many generated theorems, including
    discs ~> disc
    map_comp' ~> map_comp
    map_id' ~> map_id
    sels ~> sel
    set_map' ~> set_map
    sets ~> set
IMCOMPATIBILITY.


*** ML ***

* Spec_Check is a Quickcheck tool for Isabelle/ML.  The ML function
"check_property" allows to check specifications of the form "ALL x y
z. prop x y z".  See also ~~/src/Tools/Spec_Check/ with its
Examples.thy in particular.

* Improved printing of exception trace in Poly/ML 5.5.1, with regular
tracing output in the command transaction context instead of physical
stdout.  See also Toplevel.debug, Toplevel.debugging and
ML_Compiler.exn_trace.

  1411