Isabelle NEWS -- history user-relevant changes

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

 New in this Isabelle version

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

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

 * Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.

 Open text buffers take precedence over copies within the file-system.

 *** HOL ***

 * 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 cases: 0, 1, numeral _, - 1, - numeral _.

   * Syntax for negative numerals is mere input syntax.

 INCOMPATBILITY.

 * Elimination of fact duplicates:

     equals_zero_I ~> minus_unique

     diff_eq_0_iff_eq ~> right_minus_eq

 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.

 *** ML ***

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

 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.

 * ML type "theory" is now immutable, without any special treatment of

 drafts or linear updates (which could lead to "stale theory" errors in

 the past).  Discontinued obsolete operations like Theory.copy,

 Theory.checkpoint, and the auxiliary type theory_ref.  Minor

 INCOMPATIBILITY.

 * More uniform naming of goal functions for skipped proofs:

     Skip_Proof.prove  ~>  Goal.prove_sorry

     Skip_Proof.prove_global  ~>  Goal.prove_sorry_global

 Minor INCOMPATIBILITY.

 * Simplifier tactics and tools use proper Proof.context instead of

 historic type simpset.  Old-style declarations like addsimps,

 addsimprocs etc. operate directly on Proof.context.  Raw type simpset

 retains its use as snapshot of the main Simplifier context, using

 simpset_of and put_simpset on Proof.context.  INCOMPATIBILITY -- port

 old tools by making them depend on (ctxt : Proof.context) instead of

 (ss : simpset), then turn (simpset_of ctxt) into ctxt.

 * Modifiers for classical wrappers (e.g. addWrapper, delWrapper)

 operate on Proof.context instead of claset, for uniformity with addIs,

 addEs, addDs etc. Note that claset_of and put_claset allow to manage

 clasets separately from the context.

 * Discontinued obsolete ML antiquotations @{claset} and @{simpset}.

 INCOMPATIBILITY, use @{context} instead.

 * Antiquotation @{theory_context A} is similar to @{theory A}, but

 presents the result as initial Proof.context.

 *** System ***

 * Discontinued obsolete isabelle usedir, mkdir, make -- superseded by

 "isabelle build" in Isabelle2013.  INCOMPATIBILITY.

 * Discontinued obsolete isabelle-process options -f and -u (former

 administrative aliases of option -e).  Minor INCOMPATIBILITY.

 * Discontinued obsolete isabelle print tool, and PRINT_COMMAND

 settings variable.

 * Discontinued ISABELLE_DOC_FORMAT settings variable and historic

 document formats: dvi.gz, ps, ps.gz -- the default document format is

 always pdf.

 * Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to

 specify global resources of the JVM process run by isabelle build.

 * Toplevel executable $ISABELLE_HOME/bin/isabelle_scala_script allows

 to run Isabelle/Scala source files as standalone programs.

 * Improved "isabelle keywords" tool (for old-style ProofGeneral

 keyword tables): use Isabelle/Scala operations, which inspect outer

 syntax without requiring to build sessions first.

 * Sessions may be organized via 'chapter' specifications in the ROOT

 file, which determines a two-level hierarchy of browser info.  The old

 tree-like organization via implicit sub-session relation (with its

 tendency towards erratic fluctuation of URLs) has been discontinued.

 The default chapter is called "Unsorted".  Potential INCOMPATIBILITY

 for HTML presentation of theories.

 New in Isabelle2013 (February 2013)

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

 *** General ***

 * Theorem status about oracles and unfinished/failed future proofs is

 no longer printed by default, since it is incompatible with

 incremental / parallel checking of the persistent document model.  ML

 function Thm.peek_status may be used to inspect a snapshot of the

 ongoing evaluation process.  Note that in batch mode --- notably

 isabelle build --- the system ensures that future proofs of all

 accessible theorems in the theory context are finished (as before).

 * Configuration option show_markup controls direct inlining of markup

 into the printed representation of formal entities --- notably type

 and sort constraints.  This enables Prover IDE users to retrieve that

 information via tooltips in the output window, for example.

 * Command 'ML_file' evaluates ML text from a file directly within the

 theory, without any predeclaration via 'uses' in the theory header.

 * Old command 'use' command and corresponding keyword 'uses' in the

 theory header are legacy features and will be discontinued soon.

 Tools that load their additional source files may imitate the

 'ML_file' implementation, such that the system can take care of

 dependencies properly.

 * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which

 is called fastforce / fast_force_tac already since Isabelle2011-1.

 * Updated and extended "isar-ref" and "implementation" manual, reduced

 remaining material in old "ref" manual.

 * Improved support for auxiliary contexts that indicate block structure

 for specifications.  Nesting of "context fixes ... context assumes ..."

 and "class ... context ...".

 * Attribute "consumes" allows a negative value as well, which is

 interpreted relatively to the total number of premises of the rule in

 the target context.  This form of declaration is stable when exported

 from a nested 'context' with additional assumptions.  It is the

 preferred form for definitional packages, notably cases/rules produced

 in HOL/inductive and HOL/function.

 * More informative error messages for Isar proof commands involving

 lazy enumerations (method applications etc.).

 * Refined 'help' command to retrieve outer syntax commands according

 to name patterns (with clickable results).

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

 * Parallel terminal proofs ('by') are enabled by default, likewise

 proofs that are built into packages like 'datatype', 'function'.  This

 allows to "run ahead" checking the theory specifications on the

 surface, while the prover is still crunching on internal

 justifications.  Unfinished / cancelled proofs are restarted as

 required to complete full proof checking eventually.

 * Improved output panel with tooltips, hyperlinks etc. based on the

 same Rich_Text_Area as regular Isabelle/jEdit buffers.  Activation of

 tooltips leads to some window that supports the same recursively,

 which can lead to stacks of tooltips as the semantic document content

 is explored.  ESCAPE closes the whole stack, individual windows may be

 closed separately, or detached to become independent jEdit dockables.

 * Improved support for commands that produce graph output: the text

 message contains a clickable area to open a new instance of the graph

 browser on demand.

 * More robust incremental parsing of outer syntax (partial comments,

 malformed symbols).  Changing the balance of open/close quotes and

 comment delimiters works more conveniently with unfinished situations

 that frequently occur in user interaction.

 * More efficient painting and improved reactivity when editing large

 files.  More scalable management of formal document content.

 * Smarter handling of tracing messages: prover process pauses after

 certain number of messages per command transaction, with some user

 dialog to stop or continue.  This avoids swamping the front-end with

 potentially infinite message streams.

 * More plugin options and preferences, based on Isabelle/Scala.  The

 jEdit plugin option panel provides access to some Isabelle/Scala

 options, including tuning parameters for editor reactivity and color

 schemes.

 * Dockable window "Symbols" provides some editing support for Isabelle

 symbols.

 * Dockable window "Monitor" shows ML runtime statistics.  Note that

 continuous display of the chart slows down the system.

 * Improved editing support for control styles: subscript, superscript,

 bold, reset of style -- operating on single symbols or text

 selections.  Cf. keyboard shortcuts C+e DOWN/UP/RIGHT/LEFT.

 * Actions isabelle.increase-font-size and isabelle.decrease-font-size

 adjust the main text area font size, and its derivatives for output,

 tooltips etc.  Cf. keyboard shortcuts C-PLUS and C-MINUS, which often

 need to be adapted to local keyboard layouts.

 * More reactive completion popup by default: use \t (TAB) instead of

 \n (NEWLINE) to minimize intrusion into regular flow of editing.  See

 also "Plugin Options / SideKick / General / Code Completion Options".

 * Implicit check and build dialog of the specified logic session

 image.  For example, HOL, HOLCF, HOL-Nominal can be produced on

 demand, without bundling big platform-dependent heap images in the

 Isabelle distribution.

 * Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates

 from Oracle provide better multi-platform experience.  This version is

 now bundled exclusively with Isabelle.

 *** Pure ***

 * Code generation for Haskell: restrict unqualified imports from

 Haskell Prelude to a small set of fundamental operations.

 * Command 'export_code': relative file names are interpreted

 relatively to master directory of current theory rather than the

 rather arbitrary current working directory.  INCOMPATIBILITY.

 * Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,

 use regular rule composition via "OF" / "THEN", or explicit proof

 structure instead.  Note that Isabelle/ML provides a variety of

 operators like COMP, INCR_COMP, COMP_INCR, which need to be applied

 with some care where this is really required.

 * Command 'typ' supports an additional variant with explicit sort

 constraint, to infer and check the most general type conforming to a

 given sort.  Example (in HOL):

   typ "_ * _ * bool * unit" :: finite

 * Command 'locale_deps' visualizes all locales and their relations as

 a Hasse diagram.

 *** HOL ***

 * Sledgehammer:

   - Added MaSh relevance filter based on machine-learning; see the

     Sledgehammer manual for details.

   - Polished Isar proofs generated with "isar_proofs" option.

   - Rationalized type encodings ("type_enc" option).

   - Renamed "kill_provers" subcommand to "kill_all".

   - Renamed options:

       isar_proof ~> isar_proofs

       isar_shrink_factor ~> isar_shrink

       max_relevant ~> max_facts

       relevance_thresholds ~> fact_thresholds

 * Quickcheck: added an optimisation for equality premises.  It is

 switched on by default, and can be switched off by setting the

 configuration quickcheck_optimise_equality to false.

 * Quotient: only one quotient can be defined by quotient_type

 INCOMPATIBILITY.

 * Lifting:

   - generation of an abstraction function equation in lift_definition

   - quot_del attribute

   - renamed no_abs_code -> no_code (INCOMPATIBILITY.)

 * Simproc "finite_Collect" rewrites set comprehensions into pointfree

 expressions.

 * Preprocessing of the code generator rewrites set comprehensions into

 pointfree expressions.

 * The SMT solver Z3 has now by default a restricted set of directly

 supported features. For the full set of features (div/mod, nonlinear

 arithmetic, datatypes/records) with potential proof reconstruction

 failures, enable the configuration option "z3_with_extensions".  Minor

 INCOMPATIBILITY.

 * Simplified 'typedef' specifications: historical options for implicit

 set definition and alternative name have been discontinued.  The

 former behavior of "typedef (open) t = A" is now the default, but

 written just "typedef t = A".  INCOMPATIBILITY, need to adapt theories

 accordingly.

 * Removed constant "chars"; prefer "Enum.enum" on type "char"

 directly.  INCOMPATIBILITY.

 * Moved operation product, sublists and n_lists from theory Enum to

 List.  INCOMPATIBILITY.

 * Theorem UN_o generalized to SUP_comp.  INCOMPATIBILITY.

 * Class "comm_monoid_diff" formalises properties of bounded

 subtraction, with natural numbers and multisets as typical instances.

 * Added combinator "Option.these" with type "'a option set => 'a set".

 * Theory "Transitive_Closure": renamed lemmas

   reflcl_tranclp -> reflclp_tranclp

   rtranclp_reflcl -> rtranclp_reflclp

 INCOMPATIBILITY.

 * Theory "Rings": renamed lemmas (in class semiring)

   left_distrib ~> distrib_right

   right_distrib ~> distrib_left

 INCOMPATIBILITY.

 * Generalized the definition of limits:

   - Introduced the predicate filterlim (LIM x F. f x :> G) which

     expresses that when the input values x converge to F then the

     output f x converges to G.

   - Added filters for convergence to positive (at_top) and negative

     infinity (at_bot).

   - Moved infinity in the norm (at_infinity) from

     Multivariate_Analysis to Complex_Main.

   - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :>

     at_top".

 INCOMPATIBILITY.

 * Theory "Library/Option_ord" provides instantiation of option type to

 lattice type classes.

 * Theory "Library/Multiset": renamed

     constant fold_mset ~> Multiset.fold

     fact fold_mset_commute ~> fold_mset_comm

 INCOMPATIBILITY.

 * Renamed theory Library/List_Prefix to Library/Sublist, with related

 changes as follows.

   - Renamed constants (and related lemmas)

       prefix ~> prefixeq

       strict_prefix ~> prefix

   - Replaced constant "postfix" by "suffixeq" with swapped argument

     order (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped

     old infix syntax "xs >>= ys"; use "suffixeq ys xs" instead.

     Renamed lemmas accordingly.

   - Added constant "list_hembeq" for homeomorphic embedding on

     lists. Added abbreviation "sublisteq" for special case

     "list_hembeq (op =)".

   - Theory Library/Sublist no longer provides "order" and "bot" type

     class instances for the prefix order (merely corresponding locale

     interpretations). The type class instances are now in theory

     Library/Prefix_Order.

   - The sublist relation of theory Library/Sublist_Order is now based

     on "Sublist.sublisteq".  Renamed lemmas accordingly:

       le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff

       le_list_append_mono ~> Sublist.list_hembeq_append_mono

       le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2

       le_list_Cons_EX ~> Sublist.list_hembeq_ConsD

       le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2'

       le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq

       le_list_drop_Cons ~> Sublist.sublisteq_Cons'

       le_list_drop_many ~> Sublist.sublisteq_drop_many

       le_list_filter_left ~> Sublist.sublisteq_filter_left

       le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many

       le_list_rev_take_iff ~> Sublist.sublisteq_append

       le_list_same_length ~> Sublist.sublisteq_same_length

       le_list_take_many_iff ~> Sublist.sublisteq_append'

       less_eq_list.drop ~> less_eq_list_drop

       less_eq_list.induct ~> less_eq_list_induct

       not_le_list_length ~> Sublist.not_sublisteq_length

 INCOMPATIBILITY.

 * New theory Library/Countable_Set.

 * Theory Library/Debug and Library/Parallel provide debugging and

 parallel execution for code generated towards Isabelle/ML.

 * Theory Library/FuncSet: Extended support for Pi and extensional and

 introduce the extensional dependent function space "PiE". Replaced

 extensional_funcset by an abbreviation, and renamed lemmas from

 extensional_funcset to PiE as follows:

   extensional_empty  ~>  PiE_empty

   extensional_funcset_empty_domain  ~>  PiE_empty_domain

   extensional_funcset_empty_range  ~>  PiE_empty_range

   extensional_funcset_arb  ~>  PiE_arb

   extensional_funcset_mem  ~>  PiE_mem

   extensional_funcset_extend_domainI  ~>  PiE_fun_upd

   extensional_funcset_restrict_domain  ~>  fun_upd_in_PiE

   extensional_funcset_extend_domain_eq  ~>  PiE_insert_eq

   card_extensional_funcset  ~>  card_PiE

   finite_extensional_funcset  ~>  finite_PiE

 INCOMPATIBILITY.

 * Theory Library/FinFun: theory of almost everywhere constant

 functions (supersedes the AFP entry "Code Generation for Functions as

 Data").

 * Theory Library/Phantom: generic phantom type to make a type

 parameter appear in a constant's type.  This alternative to adding

 TYPE('a) as another parameter avoids unnecessary closures in generated

 code.

 * Theory Library/RBT_Impl: efficient construction of red-black trees

 from sorted associative lists. Merging two trees with rbt_union may

 return a structurally different tree than before.  Potential

 INCOMPATIBILITY.

 * Theory Library/IArray: immutable arrays with code generation.

 * Theory Library/Finite_Lattice: theory of finite lattices.

 * HOL/Multivariate_Analysis: replaced

   "basis :: 'a::euclidean_space => nat => real"

   "\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space"

 on euclidean spaces by using the inner product "_ \<bullet> _" with

 vectors from the Basis set: "\<Chi>\<Chi> i. f i" is superseded by

 "SUM i : Basis. f i * r i".

   With this change the following constants are also changed or removed:

     DIM('a) :: nat  ~>  card (Basis :: 'a set)   (is an abbreviation)

     a $$ i  ~>  inner a i  (where i : Basis)

     cart_base i  removed

     \<pi>, \<pi>'  removed

   Theorems about these constants where removed.

   Renamed lemmas:

     component_le_norm  ~>  Basis_le_norm

     euclidean_eq  ~>  euclidean_eq_iff

     differential_zero_maxmin_component  ~>  differential_zero_maxmin_cart

     euclidean_simps  ~>  inner_simps

     independent_basis  ~>  independent_Basis

     span_basis  ~>  span_Basis

     in_span_basis  ~>  in_span_Basis

     norm_bound_component_le  ~>  norm_boound_Basis_le

     norm_bound_component_lt  ~>  norm_boound_Basis_lt

     component_le_infnorm  ~>  Basis_le_infnorm

 INCOMPATIBILITY.

 * HOL/Probability:

   - Added simproc "measurable" to automatically prove measurability.

   - Added induction rules for sigma sets with disjoint union

     (sigma_sets_induct_disjoint) and for Borel-measurable functions

     (borel_measurable_induct).

   - Added the Daniell-Kolmogorov theorem (the existence the limit of a

     projective family).

 * HOL/Cardinals: Theories of ordinals and cardinals (supersedes the

 AFP entry "Ordinals_and_Cardinals").

 * HOL/BNF: New (co)datatype package based on bounded natural functors

 with support for mixed, nested recursion and interesting non-free

 datatypes.

 * HOL/Finite_Set and Relation: added new set and relation operations

 expressed by Finite_Set.fold.

 * New theory HOL/Library/RBT_Set: implementation of sets by red-black

 trees for the code generator.

 * HOL/Library/RBT and HOL/Library/Mapping have been converted to

 Lifting/Transfer.

 possible INCOMPATIBILITY.

 * HOL/Set: renamed Set.project -> Set.filter

 INCOMPATIBILITY.

 *** Document preparation ***

 * Dropped legacy antiquotations "term_style" and "thm_style", since

 styles may be given as arguments to "term" and "thm" already.

 Discontinued legacy styles "prem1" .. "prem19".

 * Default LaTeX rendering for \<euro> is now based on eurosym package,

 instead of slightly exotic babel/greek.

 * Document variant NAME may use different LaTeX entry point

 document/root_NAME.tex if that file exists, instead of the common

 document/root.tex.

 * Simplified custom document/build script, instead of old-style

 document/IsaMakefile.  Minor INCOMPATIBILITY.

 *** ML ***

 * The default limit for maximum number of worker threads is now 8,

 instead of 4, in correspondence to capabilities of contemporary

 hardware and Poly/ML runtime system.

 * Type Seq.results and related operations support embedded error

 messages within lazy enumerations, and thus allow to provide

 informative errors in the absence of any usable results.

 * Renamed Position.str_of to Position.here to emphasize that this is a

 formal device to inline positions into message text, but not

 necessarily printing visible text.

 *** System ***

 * Advanced support for Isabelle sessions and build management, see

 "system" manual for the chapter of that name, especially the "isabelle

 build" tool and its examples.  The "isabelle mkroot" tool prepares

 session root directories for use with "isabelle build", similar to

 former "isabelle mkdir" for "isabelle usedir".  Note that this affects

 document preparation as well.  INCOMPATIBILITY, isabelle usedir /

 mkdir / make are rendered obsolete.

 * Discontinued obsolete Isabelle/build script, it is superseded by the

 regular isabelle build tool.  For example:

   isabelle build -s -b HOL

 * Discontinued obsolete "isabelle makeall".

 * Discontinued obsolete IsaMakefile and ROOT.ML files from the

 Isabelle distribution, except for rudimentary src/HOL/IsaMakefile that

 provides some traditional targets that invoke "isabelle build".  Note

 that this is inefficient!  Applications of Isabelle/HOL involving

 "isabelle make" should be upgraded to use "isabelle build" directly.

 * The "isabelle options" tool prints Isabelle system options, as

 required for "isabelle build", for example.

 * The "isabelle logo" tool produces EPS and PDF format simultaneously.

 Minor INCOMPATIBILITY in command-line options.

 * The "isabelle install" tool has now a simpler command-line.  Minor

 INCOMPATIBILITY.

 * The "isabelle components" tool helps to resolve add-on components

 that are not bundled, or referenced from a bare-bones repository

 version of Isabelle.

 * Settings variable ISABELLE_PLATFORM_FAMILY refers to the general

 platform family: "linux", "macos", "windows".

 * The ML system is configured as regular component, and no longer

 picked up from some surrounding directory.  Potential INCOMPATIBILITY

 for home-made settings.

 * Improved ML runtime statistics (heap, threads, future tasks etc.).

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

 without exception positions and advanced ML compiler/toplevel

 configuration.

 * Discontinued special treatment of Proof General -- no longer guess

 PROOFGENERAL_HOME based on accidental file-system layout.  Minor

 INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS

 settings manually, or use a Proof General version that has been

 bundled as Isabelle component.

 New in Isabelle2012 (May 2012)

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

 *** General ***

 * Prover IDE (PIDE) improvements:

   - more robust Sledgehammer integration (as before the sledgehammer

     command-line needs to be typed into the source buffer)

   - markup for bound variables

   - markup for types of term variables (displayed as tooltips)

   - support for user-defined Isar commands within the running session

   - improved support for Unicode outside original 16bit range

     e.g. glyph for \<A> (thanks to jEdit 4.5.1)

 * Forward declaration of outer syntax keywords within the theory

 header -- minor INCOMPATIBILITY for user-defined commands.  Allow new

 commands to be used in the same theory where defined.

 * Auxiliary contexts indicate block structure for specifications with

 additional parameters and assumptions.  Such unnamed contexts may be

 nested within other targets, like 'theory', 'locale', 'class',

 'instantiation' etc.  Results from the local context are generalized

 accordingly and applied to the enclosing target context.  Example:

   context

     fixes x y z :: 'a

     assumes xy: "x = y" and yz: "y = z"

   begin

   lemma my_trans: "x = z" using xy yz by simp

   end

   thm my_trans

 The most basic application is to factor-out context elements of

 several fixes/assumes/shows theorem statements, e.g. see

 ~~/src/HOL/Isar_Examples/Group_Context.thy

 Any other local theory specification element works within the "context

 ... begin ... end" block as well.

 * Bundled declarations associate attributed fact expressions with a

 given name in the context.  These may be later included in other

 contexts.  This allows to manage context extensions casually, without

 the logical dependencies of locales and locale interpretation.  See

 commands 'bundle', 'include', 'including' etc. in the isar-ref manual.

 * Commands 'lemmas' and 'theorems' allow local variables using 'for'

 declaration, and results are standardized before being stored.  Thus

 old-style "standard" after instantiation or composition of facts

 becomes obsolete.  Minor INCOMPATIBILITY, due to potential change of

 indices of schematic variables.

 * Rule attributes in local theory declarations (e.g. locale or class)

 are now statically evaluated: the resulting theorem is stored instead

 of the original expression.  INCOMPATIBILITY in rare situations, where

 the historic accident of dynamic re-evaluation in interpretations

 etc. was exploited.

 * New tutorial "Programming and Proving in Isabelle/HOL"

 ("prog-prove").  It completely supersedes "A Tutorial Introduction to

 Structured Isar Proofs" ("isar-overview"), which has been removed.  It

 also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order

 Logic" as the recommended beginners tutorial, but does not cover all

 of the material of that old tutorial.

 * Updated and extended reference manuals: "isar-ref",

 "implementation", "system"; reduced remaining material in old "ref"

 manual.

 *** Pure ***

 * Command 'definition' no longer exports the foundational "raw_def"

 into the user context.  Minor INCOMPATIBILITY, may use the regular

 "def" result with attribute "abs_def" to imitate the old version.

 * Attribute "abs_def" turns an equation of the form "f x y == t" into

 "f == %x y. t", which ensures that "simp" or "unfold" steps always

 expand it.  This also works for object-logic equality.  (Formerly

 undocumented feature.)

 * Sort constraints are now propagated in simultaneous statements, just

 like type constraints.  INCOMPATIBILITY in rare situations, where

 distinct sorts used to be assigned accidentally.  For example:

   lemma "P (x::'a::foo)" and "Q (y::'a::bar)"  -- "now illegal"

   lemma "P (x::'a)" and "Q (y::'a::bar)"

     -- "now uniform 'a::bar instead of default sort for first occurrence (!)"

 * Rule composition via attribute "OF" (or ML functions OF/MRS) is more

 tolerant against multiple unifiers, as long as the final result is

 unique.  (As before, rules are composed in canonical right-to-left

 order to accommodate newly introduced premises.)

 * Renamed some inner syntax categories:

     num ~> num_token

     xnum ~> xnum_token

     xstr ~> str_token

 Minor INCOMPATIBILITY.  Note that in practice "num_const" or

 "num_position" etc. are mainly used instead (which also include

 position information via constraints).

 * Simplified configuration options for syntax ambiguity: see

 "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref

 manual.  Minor INCOMPATIBILITY.

 * Discontinued configuration option "syntax_positions": atomic terms

 in parse trees are always annotated by position constraints.

 * Old code generator for SML and its commands 'code_module',

 'code_library', 'consts_code', 'types_code' have been discontinued.

 Use commands of the generic code generator instead.  INCOMPATIBILITY.

 * Redundant attribute "code_inline" has been discontinued. Use

 "code_unfold" instead.  INCOMPATIBILITY.

 * Dropped attribute "code_unfold_post" in favor of the its dual

 "code_abbrev", which yields a common pattern in definitions like

   definition [code_abbrev]: "f = t"

 INCOMPATIBILITY.

 * Obsolete 'types' command has been discontinued.  Use 'type_synonym'

 instead.  INCOMPATIBILITY.

 * Discontinued old "prems" fact, which used to refer to the accidental

 collection of foundational premises in the context (already marked as

 legacy since Isabelle2011).

 *** HOL ***

 * Type 'a set is now a proper type constructor (just as before

 Isabelle2008).  Definitions mem_def and Collect_def have disappeared.

 Non-trivial INCOMPATIBILITY.  For developments keeping predicates and

 sets separate, it is often sufficient to rephrase some set S that has

 been accidentally used as predicates by "%x. x : S", and some

 predicate P that has been accidentally used as set by "{x. P x}".

 Corresponding proofs in a first step should be pruned from any

 tinkering with former theorems mem_def and Collect_def as far as

 possible.

 For developments which deliberately mix predicates and sets, a

 planning step is necessary to determine what should become a predicate

 and what a set.  It can be helpful to carry out that step in

 Isabelle2011-1 before jumping right into the current release.

 * Code generation by default implements sets as container type rather

 than predicates.  INCOMPATIBILITY.

 * New type synonym 'a rel = ('a * 'a) set

 * The representation of numerals has changed.  Datatype "num"

 represents strictly positive binary numerals, along with functions

 "numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent

 positive and negated numeric literals, respectively.  See also

 definitions in ~~/src/HOL/Num.thy.  Potential INCOMPATIBILITY, some

 user theories may require adaptations as follows:

   - Theorems with number_ring or number_semiring constraints: These

     classes are gone; use comm_ring_1 or comm_semiring_1 instead.

   - Theories defining numeric types: Remove number, number_semiring,

     and number_ring instances. Defer all theorems about numerals until

     after classes one and semigroup_add have been instantiated.

   - Numeral-only simp rules: Replace each rule having a "number_of v"

     pattern with two copies, one for numeral and one for neg_numeral.

   - Theorems about subclasses of semiring_1 or ring_1: These classes

     automatically support numerals now, so more simp rules and

     simprocs may now apply within the proof.

   - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:

     Redefine using other integer operations.

 * Transfer: New package intended to generalize the existing

 "descending" method and related theorem attributes from the Quotient

 package.  (Not all functionality is implemented yet, but future

 development will focus on Transfer as an eventual replacement for the

 corresponding parts of the Quotient package.)

   - transfer_rule attribute: Maintains a collection of transfer rules,

     which relate constants at two different types. Transfer rules may

     relate different type instances of the same polymorphic constant,

     or they may relate an operation on a raw type to a corresponding

     operation on an abstract type (quotient or subtype). For example:

     ((A ===> B) ===> list_all2 A ===> list_all2 B) map map

     (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int

   - transfer method: Replaces a subgoal on abstract types with an

     equivalent subgoal on the corresponding raw types. Constants are

     replaced with corresponding ones according to the transfer rules.

     Goals are generalized over all free variables by default; this is

     necessary for variables whose types change, but can be overridden

     for specific variables with e.g. "transfer fixing: x y z".  The

     variant transfer' method allows replacing a subgoal with one that

     is logically stronger (rather than equivalent).

   - relator_eq attribute: Collects identity laws for relators of

     various type constructors, e.g. "list_all2 (op =) = (op =)".  The

     transfer method uses these lemmas to infer transfer rules for

     non-polymorphic constants on the fly.

   - transfer_prover method: Assists with proving a transfer rule for a

     new constant, provided the constant is defined in terms of other

     constants that already have transfer rules. It should be applied

     after unfolding the constant definitions.

   - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer

     from type nat to type int.

 * Lifting: New package intended to generalize the quotient_definition

 facility of the Quotient package; designed to work with Transfer.

   - lift_definition command: Defines operations on an abstract type in

     terms of a corresponding operation on a representation

     type.  Example syntax:

     lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist"

       is List.insert

     Users must discharge a respectfulness proof obligation when each

     constant is defined. (For a type copy, i.e. a typedef with UNIV,

     the proof is discharged automatically.) The obligation is

     presented in a user-friendly, readable form; a respectfulness

     theorem in the standard format and a transfer rule are generated

     by the package.

   - Integration with code_abstype: For typedefs (e.g. subtypes

     corresponding to a datatype invariant, such as dlist),

     lift_definition generates a code certificate theorem and sets up

     code generation for each constant.

   - setup_lifting command: Sets up the Lifting package to work with a

     user-defined type. The user must provide either a quotient theorem

     or a type_definition theorem.  The package configures transfer

     rules for equality and quantifiers on the type, and sets up the

     lift_definition command to work with the type.

   - Usage examples: See Quotient_Examples/Lift_DList.thy,

     Quotient_Examples/Lift_RBT.thy, Quotient_Examples/Lift_FSet.thy,

     Word/Word.thy and Library/Float.thy.

 * Quotient package:

   - The 'quotient_type' command now supports a 'morphisms' option with

     rep and abs functions, similar to typedef.

   - 'quotient_type' sets up new types to work with the Lifting and

     Transfer packages, as with 'setup_lifting'.

   - The 'quotient_definition' command now requires the user to prove a

     respectfulness property at the point where the constant is

     defined, similar to lift_definition; INCOMPATIBILITY.

   - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems

     accordingly, INCOMPATIBILITY.

 * New diagnostic command 'find_unused_assms' to find potentially

 superfluous assumptions in theorems using Quickcheck.

 * Quickcheck:

   - Quickcheck returns variable assignments as counterexamples, which

     allows to reveal the underspecification of functions under test.

     For example, refuting "hd xs = x", it presents the variable

     assignment xs = [] and x = a1 as a counterexample, assuming that

     any property is false whenever "hd []" occurs in it.

     These counterexample are marked as potentially spurious, as

     Quickcheck also returns "xs = []" as a counterexample to the

     obvious theorem "hd xs = hd xs".

     After finding a potentially spurious counterexample, Quickcheck

     continues searching for genuine ones.

     By default, Quickcheck shows potentially spurious and genuine

     counterexamples. The option "genuine_only" sets quickcheck to only

     show genuine counterexamples.

   - The command 'quickcheck_generator' creates random and exhaustive

     value generators for a given type and operations.

     It generates values by using the operations as if they were

     constructors of that type.

   - Support for multisets.

   - Added "use_subtype" options.

   - Added "quickcheck_locale" configuration to specify how to process

     conjectures in a locale context.

 * Nitpick: Fixed infinite loop caused by the 'peephole_optim' option

 and affecting 'rat' and 'real'.

 * Sledgehammer:

   - Integrated more tightly with SPASS, as described in the ITP 2012

     paper "More SPASS with Isabelle".

   - Made it try "smt" as a fallback if "metis" fails or times out.

   - Added support for the following provers: Alt-Ergo (via Why3 and

     TFF1), iProver, iProver-Eq.

   - Sped up the minimizer.

   - Added "lam_trans", "uncurry_aliases", and "minimize" options.

   - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").

   - Renamed "sound" option to "strict".

 * Metis: Added possibility to specify lambda translations scheme as a

 parenthesized argument (e.g., "by (metis (lifting) ...)").

 * SMT: Renamed "smt_fixed" option to "smt_read_only_certificates".

 * Command 'try0': Renamed from 'try_methods'. INCOMPATIBILITY.

 * New "case_product" attribute to generate a case rule doing multiple

 case distinctions at the same time.  E.g.

   list.exhaust [case_product nat.exhaust]

 produces a rule which can be used to perform case distinction on both

 a list and a nat.

 * New "eventually_elim" method as a generalized variant of the

 eventually_elim* rules.  Supports structured proofs.

 * Typedef with implicit set definition is considered legacy.  Use

 "typedef (open)" form instead, which will eventually become the

 default.

 * Record: code generation can be switched off manually with

   declare [[record_coden = false]]  -- "default true"

 * Datatype: type parameters allow explicit sort constraints.

 * Concrete syntax for case expressions includes constraints for source

 positions, and thus produces Prover IDE markup for its bindings.

 INCOMPATIBILITY for old-style syntax translations that augment the

 pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of

 one_case.

 * Clarified attribute "mono_set": pure declaration without modifying

 the result of the fact expression.

 * More default pred/set conversions on a couple of relation operations

 and predicates.  Added powers of predicate relations.  Consolidation

 of some relation theorems:

   converse_def ~> converse_unfold

   rel_comp_def ~> relcomp_unfold

   symp_def ~> (modified, use symp_def and sym_def instead)

   transp_def ~> transp_trans

   Domain_def ~> Domain_unfold

   Range_def ~> Domain_converse [symmetric]

 Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.

 See theory "Relation" for examples for making use of pred/set

 conversions by means of attributes "to_set" and "to_pred".

 INCOMPATIBILITY.

 * Renamed facts about the power operation on relations, i.e., relpow

 to match the constant's name:

   rel_pow_1 ~> relpow_1

   rel_pow_0_I ~> relpow_0_I

   rel_pow_Suc_I ~> relpow_Suc_I

   rel_pow_Suc_I2 ~> relpow_Suc_I2

   rel_pow_0_E ~> relpow_0_E

   rel_pow_Suc_E ~> relpow_Suc_E

   rel_pow_E ~> relpow_E

   rel_pow_Suc_D2 ~> relpow_Suc_D2

   rel_pow_Suc_E2 ~> relpow_Suc_E2

   rel_pow_Suc_D2' ~> relpow_Suc_D2'

   rel_pow_E2 ~> relpow_E2

   rel_pow_add ~> relpow_add

   rel_pow_commute ~> relpow

   rel_pow_empty ~> relpow_empty:

   rtrancl_imp_UN_rel_pow ~> rtrancl_imp_UN_relpow

   rel_pow_imp_rtrancl ~> relpow_imp_rtrancl

   rtrancl_is_UN_rel_pow ~> rtrancl_is_UN_relpow

   rtrancl_imp_rel_pow ~> rtrancl_imp_relpow

   rel_pow_fun_conv ~> relpow_fun_conv

   rel_pow_finite_bounded1 ~> relpow_finite_bounded1

   rel_pow_finite_bounded ~> relpow_finite_bounded

   rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow

   trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow

   single_valued_rel_pow ~> single_valued_relpow

 INCOMPATIBILITY.

 * Theory Relation: Consolidated constant name for relation composition

 and corresponding theorem names:

   - Renamed constant rel_comp to relcomp.

   - Dropped abbreviation pred_comp. Use relcompp instead.

   - Renamed theorems:

     rel_compI ~> relcompI

     rel_compEpair ~> relcompEpair

     rel_compE ~> relcompE

     pred_comp_rel_comp_eq ~> relcompp_relcomp_eq

     rel_comp_empty1 ~> relcomp_empty1

     rel_comp_mono ~> relcomp_mono

     rel_comp_subset_Sigma ~> relcomp_subset_Sigma

     rel_comp_distrib ~> relcomp_distrib

     rel_comp_distrib2 ~> relcomp_distrib2

     rel_comp_UNION_distrib ~> relcomp_UNION_distrib

     rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2

     single_valued_rel_comp ~> single_valued_relcomp

     rel_comp_def ~> relcomp_unfold

     converse_rel_comp ~> converse_relcomp

     pred_compI ~> relcomppI

     pred_compE ~> relcomppE

     pred_comp_bot1 ~> relcompp_bot1

     pred_comp_bot2 ~> relcompp_bot2

     transp_pred_comp_less_eq ~> transp_relcompp_less_eq

     pred_comp_mono ~> relcompp_mono

     pred_comp_distrib ~> relcompp_distrib

     pred_comp_distrib2 ~> relcompp_distrib2

     converse_pred_comp ~> converse_relcompp

     finite_rel_comp ~> finite_relcomp

     set_rel_comp ~> set_relcomp

 INCOMPATIBILITY.

 * Theory Divides: Discontinued redundant theorems about div and mod.

 INCOMPATIBILITY, use the corresponding generic theorems instead.

   DIVISION_BY_ZERO ~> div_by_0, mod_by_0

   zdiv_self ~> div_self

   zmod_self ~> mod_self

   zdiv_zero ~> div_0

   zmod_zero ~> mod_0

   zdiv_zmod_equality ~> div_mod_equality2

   zdiv_zmod_equality2 ~> div_mod_equality

   zmod_zdiv_trivial ~> mod_div_trivial

   zdiv_zminus_zminus ~> div_minus_minus

   zmod_zminus_zminus ~> mod_minus_minus

   zdiv_zminus2 ~> div_minus_right

   zmod_zminus2 ~> mod_minus_right

   zdiv_minus1_right ~> div_minus1_right

   zmod_minus1_right ~> mod_minus1_right

   zdvd_mult_div_cancel ~> dvd_mult_div_cancel

   zmod_zmult1_eq ~> mod_mult_right_eq

   zpower_zmod ~> power_mod

   zdvd_zmod ~> dvd_mod

   zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd

   mod_mult_distrib ~> mult_mod_left

   mod_mult_distrib2 ~> mult_mod_right

 * Removed redundant theorems nat_mult_2 and nat_mult_2_right; use

 generic mult_2 and mult_2_right instead. INCOMPATIBILITY.

 * Finite_Set.fold now qualified.  INCOMPATIBILITY.

 * Consolidated theorem names concerning fold combinators:

   inf_INFI_fold_inf ~> inf_INF_fold_inf

   sup_SUPR_fold_sup ~> sup_SUP_fold_sup

   INFI_fold_inf ~> INF_fold_inf

   SUPR_fold_sup ~> SUP_fold_sup

   union_set ~> union_set_fold

   minus_set ~> minus_set_fold

   INFI_set_fold ~> INF_set_fold

   SUPR_set_fold ~> SUP_set_fold

   INF_code ~> INF_set_foldr

   SUP_code ~> SUP_set_foldr

   foldr.simps ~> foldr.simps (in point-free formulation)

   foldr_fold_rev ~> foldr_conv_fold

   foldl_fold ~> foldl_conv_fold

   foldr_foldr ~> foldr_conv_foldl

   foldl_foldr ~> foldl_conv_foldr

   fold_set_remdups ~> fold_set_fold_remdups

   fold_set ~> fold_set_fold

   fold1_set ~> fold1_set_fold

 INCOMPATIBILITY.

 * Dropped rarely useful theorems concerning fold combinators:

 foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,

 rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,

 concat_conv_foldl, foldl_weak_invariant, foldl_invariant,

 foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,

 listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,

 foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.

 INCOMPATIBILITY.  For the common phrases "%xs. List.foldr plus xs 0"

 and "List.foldl plus 0", prefer "List.listsum".  Otherwise it can be

 useful to boil down "List.foldr" and "List.foldl" to "List.fold" by

 unfolding "foldr_conv_fold" and "foldl_conv_fold".

 * Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,

 inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,

 Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,

 INF_set_foldr, SUP_set_foldr.  INCOMPATIBILITY.  Prefer corresponding

 lemmas over fold rather than foldr, or make use of lemmas

 fold_conv_foldr and fold_rev.

 * Congruence rules Option.map_cong and Option.bind_cong for recursion

 through option types.

 * "Transitive_Closure.ntrancl": bounded transitive closure on

 relations.

 * Constant "Set.not_member" now qualified.  INCOMPATIBILITY.

 * Theory Int: Discontinued many legacy theorems specific to type int.

 INCOMPATIBILITY, use the corresponding generic theorems instead.

   zminus_zminus ~> minus_minus

   zminus_0 ~> minus_zero

   zminus_zadd_distrib ~> minus_add_distrib

   zadd_commute ~> add_commute

   zadd_assoc ~> add_assoc

   zadd_left_commute ~> add_left_commute

   zadd_ac ~> add_ac

   zmult_ac ~> mult_ac

   zadd_0 ~> add_0_left

   zadd_0_right ~> add_0_right

   zadd_zminus_inverse2 ~> left_minus

   zmult_zminus ~> mult_minus_left

   zmult_commute ~> mult_commute

   zmult_assoc ~> mult_assoc

   zadd_zmult_distrib ~> left_distrib

   zadd_zmult_distrib2 ~> right_distrib

   zdiff_zmult_distrib ~> left_diff_distrib

   zdiff_zmult_distrib2 ~> right_diff_distrib

   zmult_1 ~> mult_1_left

   zmult_1_right ~> mult_1_right

   zle_refl ~> order_refl

   zle_trans ~> order_trans

   zle_antisym ~> order_antisym

   zle_linear ~> linorder_linear

   zless_linear ~> linorder_less_linear

   zadd_left_mono ~> add_left_mono

   zadd_strict_right_mono ~> add_strict_right_mono

   zadd_zless_mono ~> add_less_le_mono

   int_0_less_1 ~> zero_less_one

   int_0_neq_1 ~> zero_neq_one

   zless_le ~> less_le

   zpower_zadd_distrib ~> power_add

   zero_less_zpower_abs_iff ~> zero_less_power_abs_iff

   zero_le_zpower_abs ~> zero_le_power_abs

 * Theory Deriv: Renamed

   DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing

 * Theory Library/Multiset: Improved code generation of multisets.

 * Theory HOL/Library/Set_Algebras: Addition and multiplication on sets

 are expressed via type classes again. The special syntax

 \<oplus>/\<otimes> has been replaced by plain +/*. Removed constant

 setsum_set, which is now subsumed by Big_Operators.setsum.

 INCOMPATIBILITY.

 * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,

 use theory HOL/Library/Nat_Bijection instead.

 * Theory HOL/Library/RBT_Impl: Backing implementation of red-black

 trees is now inside a type class context.  Names of affected

 operations and lemmas have been prefixed by rbt_.  INCOMPATIBILITY for

 theories working directly with raw red-black trees, adapt the names as

 follows:

   Operations:

   bulkload -> rbt_bulkload

   del_from_left -> rbt_del_from_left

   del_from_right -> rbt_del_from_right

   del -> rbt_del

   delete -> rbt_delete

   ins -> rbt_ins

   insert -> rbt_insert

   insertw -> rbt_insert_with

   insert_with_key -> rbt_insert_with_key

   map_entry -> rbt_map_entry

   lookup -> rbt_lookup

   sorted -> rbt_sorted

   tree_greater -> rbt_greater

   tree_less -> rbt_less

   tree_less_symbol -> rbt_less_symbol

   union -> rbt_union

   union_with -> rbt_union_with

   union_with_key -> rbt_union_with_key

   Lemmas:

   balance_left_sorted -> balance_left_rbt_sorted

   balance_left_tree_greater -> balance_left_rbt_greater

   balance_left_tree_less -> balance_left_rbt_less

   balance_right_sorted -> balance_right_rbt_sorted

   balance_right_tree_greater -> balance_right_rbt_greater

   balance_right_tree_less -> balance_right_rbt_less

   balance_sorted -> balance_rbt_sorted

   balance_tree_greater -> balance_rbt_greater

   balance_tree_less -> balance_rbt_less

   bulkload_is_rbt -> rbt_bulkload_is_rbt

   combine_sorted -> combine_rbt_sorted

   combine_tree_greater -> combine_rbt_greater

   combine_tree_less -> combine_rbt_less

   delete_in_tree -> rbt_delete_in_tree

   delete_is_rbt -> rbt_delete_is_rbt

   del_from_left_tree_greater -> rbt_del_from_left_rbt_greater

   del_from_left_tree_less -> rbt_del_from_left_rbt_less

   del_from_right_tree_greater -> rbt_del_from_right_rbt_greater

   del_from_right_tree_less -> rbt_del_from_right_rbt_less

   del_in_tree -> rbt_del_in_tree

   del_inv1_inv2 -> rbt_del_inv1_inv2

   del_sorted -> rbt_del_rbt_sorted

   del_tree_greater -> rbt_del_rbt_greater

   del_tree_less -> rbt_del_rbt_less

   dom_lookup_Branch -> dom_rbt_lookup_Branch

   entries_lookup -> entries_rbt_lookup

   finite_dom_lookup -> finite_dom_rbt_lookup

   insert_sorted -> rbt_insert_rbt_sorted

   insertw_is_rbt -> rbt_insertw_is_rbt

   insertwk_is_rbt -> rbt_insertwk_is_rbt

   insertwk_sorted -> rbt_insertwk_rbt_sorted

   insertw_sorted -> rbt_insertw_rbt_sorted

   ins_sorted -> ins_rbt_sorted

   ins_tree_greater -> ins_rbt_greater

   ins_tree_less -> ins_rbt_less

   is_rbt_sorted -> is_rbt_rbt_sorted

   lookup_balance -> rbt_lookup_balance

   lookup_bulkload -> rbt_lookup_rbt_bulkload

   lookup_delete -> rbt_lookup_rbt_delete

   lookup_Empty -> rbt_lookup_Empty

   lookup_from_in_tree -> rbt_lookup_from_in_tree

   lookup_in_tree -> rbt_lookup_in_tree

   lookup_ins -> rbt_lookup_ins

   lookup_insert -> rbt_lookup_rbt_insert

   lookup_insertw -> rbt_lookup_rbt_insertw

   lookup_insertwk -> rbt_lookup_rbt_insertwk

   lookup_keys -> rbt_lookup_keys

   lookup_map -> rbt_lookup_map

   lookup_map_entry -> rbt_lookup_rbt_map_entry

   lookup_tree_greater -> rbt_lookup_rbt_greater

   lookup_tree_less -> rbt_lookup_rbt_less

   lookup_union -> rbt_lookup_rbt_union

   map_entry_color_of -> rbt_map_entry_color_of

   map_entry_inv1 -> rbt_map_entry_inv1

   map_entry_inv2 -> rbt_map_entry_inv2

   map_entry_is_rbt -> rbt_map_entry_is_rbt

   map_entry_sorted -> rbt_map_entry_rbt_sorted

   map_entry_tree_greater -> rbt_map_entry_rbt_greater

   map_entry_tree_less -> rbt_map_entry_rbt_less

   map_tree_greater -> map_rbt_greater

   map_tree_less -> map_rbt_less

   map_sorted -> map_rbt_sorted

   paint_sorted -> paint_rbt_sorted

   paint_lookup -> paint_rbt_lookup

   paint_tree_greater -> paint_rbt_greater

   paint_tree_less -> paint_rbt_less

   sorted_entries -> rbt_sorted_entries

   tree_greater_eq_trans -> rbt_greater_eq_trans

   tree_greater_nit -> rbt_greater_nit

   tree_greater_prop -> rbt_greater_prop

   tree_greater_simps -> rbt_greater_simps

   tree_greater_trans -> rbt_greater_trans

   tree_less_eq_trans -> rbt_less_eq_trans

   tree_less_nit -> rbt_less_nit

   tree_less_prop -> rbt_less_prop

   tree_less_simps -> rbt_less_simps

   tree_less_trans -> rbt_less_trans

   tree_ord_props -> rbt_ord_props

   union_Branch -> rbt_union_Branch

   union_is_rbt -> rbt_union_is_rbt

   unionw_is_rbt -> rbt_unionw_is_rbt

   unionwk_is_rbt -> rbt_unionwk_is_rbt

   unionwk_sorted -> rbt_unionwk_rbt_sorted

 * Theory HOL/Library/Float: Floating point numbers are now defined as

 a subset of the real numbers.  All operations are defined using the

 lifing-framework and proofs use the transfer method.  INCOMPATIBILITY.

   Changed Operations:

   float_abs -> abs

   float_nprt -> nprt

   float_pprt -> pprt

   pow2 -> use powr

   round_down -> float_round_down

   round_up -> float_round_up

   scale -> exponent

   Removed Operations:

   ceiling_fl, lb_mult, lb_mod, ub_mult, ub_mod

   Renamed Lemmas:

   abs_float_def -> Float.compute_float_abs

   bitlen_ge0 -> bitlen_nonneg

   bitlen.simps -> Float.compute_bitlen

   float_components -> Float_mantissa_exponent

   float_divl.simps -> Float.compute_float_divl

   float_divr.simps -> Float.compute_float_divr

   float_eq_odd -> mult_powr_eq_mult_powr_iff

   float_power -> real_of_float_power

   lapprox_posrat_def -> Float.compute_lapprox_posrat

   lapprox_rat.simps -> Float.compute_lapprox_rat

   le_float_def' -> Float.compute_float_le

   le_float_def -> less_eq_float.rep_eq

   less_float_def' -> Float.compute_float_less

   less_float_def -> less_float.rep_eq

   normfloat_def -> Float.compute_normfloat

   normfloat_imp_odd_or_zero -> mantissa_not_dvd and mantissa_noteq_0

   normfloat -> normfloat_def

   normfloat_unique -> use normfloat_def

   number_of_float_Float -> Float.compute_float_numeral, Float.compute_float_neg_numeral

   one_float_def -> Float.compute_float_one

   plus_float_def -> Float.compute_float_plus

   rapprox_posrat_def -> Float.compute_rapprox_posrat

   rapprox_rat.simps -> Float.compute_rapprox_rat

   real_of_float_0 -> zero_float.rep_eq

   real_of_float_1 -> one_float.rep_eq

   real_of_float_abs -> abs_float.rep_eq

   real_of_float_add -> plus_float.rep_eq

   real_of_float_minus -> uminus_float.rep_eq

   real_of_float_mult -> times_float.rep_eq

   real_of_float_simp -> Float.rep_eq

   real_of_float_sub -> minus_float.rep_eq

   round_down.simps -> Float.compute_float_round_down

   round_up.simps -> Float.compute_float_round_up

   times_float_def -> Float.compute_float_times

   uminus_float_def -> Float.compute_float_uminus

   zero_float_def -> Float.compute_float_zero

   Lemmas not necessary anymore, use the transfer method:

   bitlen_B0, bitlen_B1, bitlen_ge1, bitlen_Min, bitlen_Pls, float_divl,

   float_divr, float_le_simp, float_less1_mantissa_bound,

   float_less_simp, float_less_zero, float_le_zero,

   float_pos_less1_e_neg, float_pos_m_pos, float_split, float_split2,

   floor_pos_exp, lapprox_posrat, lapprox_posrat_bottom, lapprox_rat,

   lapprox_rat_bottom, normalized_float, rapprox_posrat,

   rapprox_posrat_le1, rapprox_rat, real_of_float_ge0_exp,

   real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl,

   round_up, zero_le_float, zero_less_float

 * New theory HOL/Library/DAList provides an abstract type for

 association lists with distinct keys.

 * Session HOL/IMP: Added new theory of abstract interpretation of

 annotated commands.

 * Session HOL-Import: Re-implementation from scratch is faster,

 simpler, and more scalable.  Requires a proof bundle, which is

 available as an external component.  Discontinued old (and mostly

 dead) Importer for HOL4 and HOL Light.  INCOMPATIBILITY.

 * Session HOL-Word: Discontinued many redundant theorems specific to

 type 'a word. INCOMPATIBILITY, use the corresponding generic theorems

 instead.

   word_sub_alt ~> word_sub_wi

   word_add_alt ~> word_add_def

   word_mult_alt ~> word_mult_def

   word_minus_alt ~> word_minus_def

   word_0_alt ~> word_0_wi

   word_1_alt ~> word_1_wi

   word_add_0 ~> add_0_left

   word_add_0_right ~> add_0_right

   word_mult_1 ~> mult_1_left

   word_mult_1_right ~> mult_1_right

   word_add_commute ~> add_commute

   word_add_assoc ~> add_assoc

   word_add_left_commute ~> add_left_commute

   word_mult_commute ~> mult_commute

   word_mult_assoc ~> mult_assoc

   word_mult_left_commute ~> mult_left_commute

   word_left_distrib ~> left_distrib

   word_right_distrib ~> right_distrib

   word_left_minus ~> left_minus

   word_diff_0_right ~> diff_0_right

   word_diff_self ~> diff_self

   word_sub_def ~> diff_minus

   word_diff_minus ~> diff_minus

   word_add_ac ~> add_ac

   word_mult_ac ~> mult_ac

   word_plus_ac0 ~> add_0_left add_0_right add_ac

   word_times_ac1 ~> mult_1_left mult_1_right mult_ac

   word_order_trans ~> order_trans

   word_order_refl ~> order_refl

   word_order_antisym ~> order_antisym

   word_order_linear ~> linorder_linear

   lenw1_zero_neq_one ~> zero_neq_one

   word_number_of_eq ~> number_of_eq

   word_of_int_add_hom ~> wi_hom_add

   word_of_int_sub_hom ~> wi_hom_sub

   word_of_int_mult_hom ~> wi_hom_mult

   word_of_int_minus_hom ~> wi_hom_neg

   word_of_int_succ_hom ~> wi_hom_succ

   word_of_int_pred_hom ~> wi_hom_pred

   word_of_int_0_hom ~> word_0_wi

   word_of_int_1_hom ~> word_1_wi

 * Session HOL-Word: New proof method "word_bitwise" for splitting

 machine word equalities and inequalities into logical circuits,

 defined in HOL/Word/WordBitwise.thy.  Supports addition, subtraction,

 multiplication, shifting by constants, bitwise operators and numeric

 constants.  Requires fixed-length word types, not 'a word.  Solves

 many standard word identities outright and converts more into first

 order problems amenable to blast or similar.  See also examples in

 HOL/Word/Examples/WordExamples.thy.

 * Session HOL-Probability: Introduced the type "'a measure" to

 represent measures, this replaces the records 'a algebra and 'a

 measure_space.  The locales based on subset_class now have two

 locale-parameters the space \<Omega> and the set of measurable sets M.

 The product of probability spaces uses now the same constant as the

 finite product of sigma-finite measure spaces "PiM :: ('i => 'a)

 measure".  Most constants are defined now outside of locales and gain

 an additional parameter, like null_sets, almost_eventually or \<mu>'.

 Measure space constructions for distributions and densities now got

 their own constants distr and density.  Instead of using locales to

 describe measure spaces with a finite space, the measure count_space

 and point_measure is introduced.  INCOMPATIBILITY.

   Renamed constants:

   measure -> emeasure

   finite_measure.\<mu>' -> measure

   product_algebra_generator -> prod_algebra

   product_prob_space.emb -> prod_emb

   product_prob_space.infprod_algebra -> PiM

   Removed locales:

   completeable_measure_space

   finite_measure_space

   finite_prob_space

   finite_product_finite_prob_space

   finite_product_sigma_algebra

   finite_sigma_algebra

   measure_space

   pair_finite_prob_space

   pair_finite_sigma_algebra

   pair_finite_space

   pair_sigma_algebra

   product_sigma_algebra

   Removed constants:

   conditional_space

   distribution -> use distr measure, or distributed predicate

   image_space

   joint_distribution -> use distr measure, or distributed predicate

   pair_measure_generator

   product_prob_space.infprod_algebra -> use PiM

   subvimage

   Replacement theorems:

   finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite

   finite_measure.empty_measure -> measure_empty

   finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq

   finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq

   finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably

   finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure

   finite_measure.finite_measure -> finite_measure.emeasure_finite

   finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton

   finite_measure.positive_measure' -> measure_nonneg

   finite_measure.real_measure -> finite_measure.emeasure_real

   finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb

   finite_product_sigma_algebra.in_P -> sets_PiM_I_finite

   finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty

   information_space.conditional_entropy_eq -> information_space.conditional_entropy_simple_distributed

   information_space.conditional_entropy_positive -> information_space.conditional_entropy_nonneg_simple

   information_space.conditional_mutual_information_eq_mutual_information -> information_space.conditional_mutual_information_eq_mutual_information_simple

   information_space.conditional_mutual_information_generic_positive -> information_space.conditional_mutual_information_nonneg_simple

   information_space.conditional_mutual_information_positive -> information_space.conditional_mutual_information_nonneg_simple

   information_space.entropy_commute -> information_space.entropy_commute_simple

   information_space.entropy_eq -> information_space.entropy_simple_distributed

   information_space.entropy_generic_eq -> information_space.entropy_simple_distributed

   information_space.entropy_positive -> information_space.entropy_nonneg_simple

   information_space.entropy_uniform_max -> information_space.entropy_uniform

   information_space.KL_eq_0_imp -> information_space.KL_eq_0_iff_eq

   information_space.KL_eq_0 -> information_space.KL_same_eq_0

   information_space.KL_ge_0 -> information_space.KL_nonneg

   information_space.mutual_information_eq -> information_space.mutual_information_simple_distributed

   information_space.mutual_information_positive -> information_space.mutual_information_nonneg_simple

   Int_stable_cuboids -> Int_stable_atLeastAtMost

   Int_stable_product_algebra_generator -> positive_integral

   measure_preserving -> equality "distr M N f = N" "f : measurable M N"

   measure_space.additive -> emeasure_additive

   measure_space.AE_iff_null_set -> AE_iff_null

   measure_space.almost_everywhere_def -> eventually_ae_filter

   measure_space.almost_everywhere_vimage -> AE_distrD

   measure_space.continuity_from_above -> INF_emeasure_decseq

   measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq

   measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq

   measure_space.continuity_from_below -> SUP_emeasure_incseq

   measure_space_density -> emeasure_density

   measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density

   measure_space.integrable_vimage -> integrable_distr

   measure_space.integral_translated_density -> integral_density

   measure_space.integral_vimage -> integral_distr

   measure_space.measure_additive -> plus_emeasure

   measure_space.measure_compl -> emeasure_compl

   measure_space.measure_countable_increasing -> emeasure_countable_increasing

   measure_space.measure_countably_subadditive -> emeasure_subadditive_countably

   measure_space.measure_decseq -> decseq_emeasure

   measure_space.measure_Diff -> emeasure_Diff

   measure_space.measure_Diff_null_set -> emeasure_Diff_null_set

   measure_space.measure_eq_0 -> emeasure_eq_0

   measure_space.measure_finitely_subadditive -> emeasure_subadditive_finite

   measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton

   measure_space.measure_incseq -> incseq_emeasure

   measure_space.measure_insert -> emeasure_insert

   measure_space.measure_mono -> emeasure_mono

   measure_space.measure_not_negative -> emeasure_not_MInf

   measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq

   measure_space.measure_setsum -> setsum_emeasure

   measure_space.measure_setsum_split -> setsum_emeasure_cover

   measure_space.measure_space_vimage -> emeasure_distr

   measure_space.measure_subadditive_finite -> emeasure_subadditive_finite

   measure_space.measure_subadditive -> subadditive

   measure_space.measure_top -> emeasure_space

   measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0

   measure_space.measure_Un_null_set -> emeasure_Un_null_set

   measure_space.positive_integral_translated_density -> positive_integral_density

   measure_space.positive_integral_vimage -> positive_integral_distr

   measure_space.real_continuity_from_above -> Lim_measure_decseq

   measure_space.real_continuity_from_below -> Lim_measure_incseq

   measure_space.real_measure_countably_subadditive -> measure_subadditive_countably

   measure_space.real_measure_Diff -> measure_Diff

   measure_space.real_measure_finite_Union -> measure_finite_Union

   measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton

   measure_space.real_measure_subadditive -> measure_subadditive

   measure_space.real_measure_Union -> measure_Union

   measure_space.real_measure_UNION -> measure_UNION

   measure_space.simple_function_vimage -> simple_function_comp

   measure_space.simple_integral_vimage -> simple_integral_distr

   measure_space.simple_integral_vimage -> simple_integral_distr

   measure_unique_Int_stable -> measure_eqI_generator_eq

   measure_unique_Int_stable_vimage -> measure_eqI_generator_eq

   pair_sigma_algebra.measurable_cut_fst -> sets_Pair1

   pair_sigma_algebra.measurable_cut_snd -> sets_Pair2

   pair_sigma_algebra.measurable_pair_image_fst -> measurable_Pair1

   pair_sigma_algebra.measurable_pair_image_snd -> measurable_Pair2

   pair_sigma_algebra.measurable_product_swap -> measurable_pair_swap_iff

   pair_sigma_algebra.pair_sigma_algebra_measurable -> measurable_pair_swap

   pair_sigma_algebra.pair_sigma_algebra_swap_measurable -> measurable_pair_swap'

   pair_sigma_algebra.sets_swap -> sets_pair_swap

   pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1

   pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2

   pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap

   pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2

   pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt

   pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times

   prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM

   prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq

   prob_space.measure_space_1 -> prob_space.emeasure_space_1

   prob_space.prob_space_vimage -> prob_space_distr

   prob_space.random_variable_restrict -> measurable_restrict

   prob_space_unique_Int_stable -> measure_eqI_prob_space

   product_algebraE -> prod_algebraE_all

   product_algebra_generator_der -> prod_algebra_eq_finite

   product_algebra_generator_into_space -> prod_algebra_sets_into_space

   product_algebraI -> sets_PiM_I_finite

   product_measure_exists -> product_sigma_finite.sigma_finite

   product_prob_space.finite_index_eq_finite_product -> product_prob_space.sets_PiM_generator

   product_prob_space.finite_measure_infprod_emb_Pi -> product_prob_space.measure_PiM_emb

   product_prob_space.infprod_spec -> product_prob_space.emeasure_PiM_emb_not_empty

   product_prob_space.measurable_component -> measurable_component_singleton

   product_prob_space.measurable_emb -> measurable_prod_emb

   product_prob_space.measurable_into_infprod_algebra -> measurable_PiM_single

   product_prob_space.measurable_singleton_infprod -> measurable_component_singleton

   product_prob_space.measure_emb -> emeasure_prod_emb

   product_prob_space.measure_preserving_restrict -> product_prob_space.distr_restrict

   product_sigma_algebra.product_algebra_into_space -> space_closed

   product_sigma_finite.measure_fold -> product_sigma_finite.distr_merge

   product_sigma_finite.measure_preserving_component_singelton -> product_sigma_finite.distr_singleton

   product_sigma_finite.measure_preserving_merge -> product_sigma_finite.distr_merge

   sequence_space.measure_infprod -> sequence_space.measure_PiM_countable

   sets_product_algebra -> sets_PiM

   sigma_algebra.measurable_sigma -> measurable_measure_of

   sigma_finite_measure.disjoint_sigma_finite -> sigma_finite_disjoint

   sigma_finite_measure.RN_deriv_vimage -> sigma_finite_measure.RN_deriv_distr

   sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq

   space_product_algebra -> space_PiM

 * Session HOL-TPTP: support to parse and import TPTP problems (all

 languages) into Isabelle/HOL.

 *** FOL ***

 * New "case_product" attribute (see HOL).

 *** ZF ***

 * Greater support for structured proofs involving induction or case

 analysis.

 * Much greater use of mathematical symbols.

 * Removal of many ML theorem bindings.  INCOMPATIBILITY.

 *** ML ***

 * Antiquotation @{keyword "name"} produces a parser for outer syntax

 from a minor keyword introduced via theory header declaration.

 * Antiquotation @{command_spec "name"} produces the

 Outer_Syntax.command_spec from a major keyword introduced via theory

 header declaration; it can be passed to Outer_Syntax.command etc.

 * Local_Theory.define no longer hard-wires default theorem name

 "foo_def", but retains the binding as given.  If that is Binding.empty

 / Attrib.empty_binding, the result is not registered as user-level

 fact.  The Local_Theory.define_internal variant allows to specify a

 non-empty name (used for the foundation in the background theory),

 while omitting the fact binding in the user-context.  Potential

 INCOMPATIBILITY for derived definitional packages: need to specify

 naming policy for primitive definitions more explicitly.

 * Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in

 conformance with similar operations in structure Term and Logic.

 * Antiquotation @{attributes [...]} embeds attribute source

 representation into the ML text, which is particularly useful with

 declarations like Local_Theory.note.

 * Structure Proof_Context follows standard naming scheme.  Old

 ProofContext has been discontinued.  INCOMPATIBILITY.

 * Refined Local_Theory.declaration {syntax, pervasive}, with subtle

 change of semantics: update is applied to auxiliary local theory

 context as well.

 * Modernized some old-style infix operations:

   addeqcongs    ~> Simplifier.add_eqcong

   deleqcongs    ~> Simplifier.del_eqcong

   addcongs      ~> Simplifier.add_cong

   delcongs      ~> Simplifier.del_cong

   setmksimps    ~> Simplifier.set_mksimps

   setmkcong     ~> Simplifier.set_mkcong

   setmksym      ~> Simplifier.set_mksym

   setmkeqTrue   ~> Simplifier.set_mkeqTrue

   settermless   ~> Simplifier.set_termless

   setsubgoaler  ~> Simplifier.set_subgoaler

   addsplits     ~> Splitter.add_split

   delsplits     ~> Splitter.del_split

 *** System ***

 * USER_HOME settings variable points to cross-platform user home

 directory, which coincides with HOME on POSIX systems only.  Likewise,

 the Isabelle path specification "~" now expands to $USER_HOME, instead

 of former $HOME.  A different default for USER_HOME may be set

 explicitly in shell environment, before Isabelle settings are

 evaluated.  Minor INCOMPATIBILITY: need to adapt Isabelle path where

 the generic user home was intended.

 * ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name

 notation, which is useful for the jEdit file browser, for example.

 * ISABELLE_JDK_HOME settings variable points to JDK with javac and jar

 (not just JRE).

 New in Isabelle2011-1 (October 2011)

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

 *** General ***

 * Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as

 "isabelle jedit" or "ISABELLE_HOME/Isabelle" on the command line.

   - Management of multiple theory files directly from the editor

     buffer store -- bypassing the file-system (no requirement to save

     files for checking).

   - Markup of formal entities within the text buffer, with semantic

     highlighting, tooltips and hyperlinks to jump to defining source

     positions.

   - Improved text rendering, with sub/superscripts in the source

     buffer (including support for copy/paste wrt. output panel, HTML

     theory output and other non-Isabelle text boxes).

   - Refined scheduling of proof checking and printing of results,

     based on interactive editor view.  (Note: jEdit folding and

     narrowing allows to restrict buffer perspectives explicitly.)

   - Reduced CPU performance requirements, usable on machines with few

     cores.

   - Reduced memory requirements due to pruning of unused document

     versions (garbage collection).

 See also ~~/src/Tools/jEdit/README.html for further information,

 including some remaining limitations.

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

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

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

 Note that the path element ~~ may be used to reference theories in the

 Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet".

 INCOMPATIBILITY.

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

 digests.  Discontinued former path/modtime identification and optional

 ISABELLE_FILE_IDENT plugin scripts.

 * Parallelization of nested Isar proofs is subject to

 Goal.parallel_proofs_threshold (default 100).  See also isabelle

 usedir option -Q.

 * Name space: former unsynchronized references are now proper

 configuration options, with more conventional names:

   long_names   ~> names_long

   short_names  ~> names_short

   unique_names ~> names_unique

 Minor INCOMPATIBILITY, need to declare options in context like this:

   declare [[names_unique = false]]

 * Literal facts `prop` may contain dummy patterns, e.g. `_ = _`.  Note

 that the result needs to be unique, which means fact specifications

 may have to be refined after enriching a proof context.

 * Attribute "case_names" has been refined: the assumptions in each case

 can be named now by following the case name with [name1 name2 ...].

 * Isabelle/Isar reference manual has been updated and extended:

   - "Synopsis" provides a catalog of main Isar language concepts.

   - Formal references in syntax diagrams, via @{rail} antiquotation.

   - Updated material from classic "ref" manual, notably about

     "Classical Reasoner".

 *** HOL ***

 * Class bot and top require underlying partial order rather than

 preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.

 * Class complete_lattice: generalized a couple of lemmas from sets;

 generalized theorems INF_cong and SUP_cong.  New type classes for

 complete boolean algebras and complete linear orders.  Lemmas

 Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in

 class complete_linorder.

 Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def,

 Sup_fun_def, Inf_apply, Sup_apply.

 Removed redundant lemmas (the right hand side gives hints how to

 replace them for (metis ...), or (simp only: ...) proofs):

   Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right]

   Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right]

   Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right

   Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right

   Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right

   Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right

   Inter_def ~> INF_def, image_def

   Union_def ~> SUP_def, image_def

   INT_eq ~> INF_def, and image_def

   UN_eq ~> SUP_def, and image_def

   INF_subset ~> INF_superset_mono [OF _ order_refl]

 More consistent and comprehensive names:

   INTER_eq_Inter_image ~> INF_def

   UNION_eq_Union_image ~> SUP_def

   INFI_def ~> INF_def

   SUPR_def ~> SUP_def

   INF_leI ~> INF_lower

   INF_leI2 ~> INF_lower2

   le_INFI ~> INF_greatest

   le_SUPI ~> SUP_upper

   le_SUPI2 ~> SUP_upper2

   SUP_leI ~> SUP_least

   INFI_bool_eq ~> INF_bool_eq

   SUPR_bool_eq ~> SUP_bool_eq

   INFI_apply ~> INF_apply

   SUPR_apply ~> SUP_apply

   INTER_def ~> INTER_eq

   UNION_def ~> UNION_eq

 INCOMPATIBILITY.

 * Renamed theory Complete_Lattice to Complete_Lattices.

 INCOMPATIBILITY.

 * Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff,

 INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot,

 Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image,

 Sup_insert are now declared as [simp].  INCOMPATIBILITY.

 * Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff,

 compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem,

 sup_inf_absob, sup_left_idem are now declared as [simp].  Minor

 INCOMPATIBILITY.

 * Added syntactic classes "inf" and "sup" for the respective

 constants.  INCOMPATIBILITY: Changes in the argument order of the

 (mostly internal) locale predicates for some derived classes.

 * Theorem collections ball_simps and bex_simps do not contain theorems

 referring to UNION any longer; these have been moved to collection

 UN_ball_bex_simps.  INCOMPATIBILITY.

 * Theory Archimedean_Field: floor now is defined as parameter of a

 separate type class floor_ceiling.

 * Theory Finite_Set: more coherent development of fold_set locales:

     locale fun_left_comm ~> locale comp_fun_commute

     locale fun_left_comm_idem ~> locale comp_fun_idem

 Both use point-free characterization; interpretation proofs may need

 adjustment.  INCOMPATIBILITY.

 * Theory Limits: Type "'a net" has been renamed to "'a filter", in

 accordance with standard mathematical terminology. INCOMPATIBILITY.

 * Theory Complex_Main: The locale interpretations for the

 bounded_linear and bounded_bilinear locales have been removed, in

 order to reduce the number of duplicate lemmas. Users must use the

 original names for distributivity theorems, potential INCOMPATIBILITY.

   divide.add ~> add_divide_distrib

   divide.diff ~> diff_divide_distrib

   divide.setsum ~> setsum_divide_distrib

   mult.add_right ~> right_distrib

   mult.diff_right ~> right_diff_distrib

   mult_right.setsum ~> setsum_right_distrib

   mult_left.diff ~> left_diff_distrib

 * Theory Complex_Main: Several redundant theorems have been removed or

 replaced by more general versions. INCOMPATIBILITY.

   real_diff_def ~> minus_real_def

   real_divide_def ~> divide_real_def

   real_less_def ~> less_le

   real_abs_def ~> abs_real_def

   real_sgn_def ~> sgn_real_def

   real_mult_commute ~> mult_commute

   real_mult_assoc ~> mult_assoc

   real_mult_1 ~> mult_1_left

   real_add_mult_distrib ~> left_distrib

   real_zero_not_eq_one ~> zero_neq_one

   real_mult_inverse_left ~> left_inverse

   INVERSE_ZERO ~> inverse_zero

   real_le_refl ~> order_refl

   real_le_antisym ~> order_antisym

   real_le_trans ~> order_trans

   real_le_linear ~> linear

   real_le_eq_diff ~> le_iff_diff_le_0

   real_add_left_mono ~> add_left_mono

   real_mult_order ~> mult_pos_pos

   real_mult_less_mono2 ~> mult_strict_left_mono

   real_of_int_real_of_nat ~> real_of_int_of_nat_eq

   real_0_le_divide_iff ~> zero_le_divide_iff

   realpow_two_disj ~> power2_eq_iff

   real_squared_diff_one_factored ~> square_diff_one_factored

   realpow_two_diff ~> square_diff_square_factored

   reals_complete2 ~> complete_real

   real_sum_squared_expand ~> power2_sum

   exp_ln_eq ~> ln_unique

   expi_add ~> exp_add

   expi_zero ~> exp_zero

   lemma_DERIV_subst ~> DERIV_cong

   LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff

   LIMSEQ_const ~> tendsto_const

   LIMSEQ_norm ~> tendsto_norm

   LIMSEQ_add ~> tendsto_add

   LIMSEQ_minus ~> tendsto_minus

   LIMSEQ_minus_cancel ~> tendsto_minus_cancel

   LIMSEQ_diff ~> tendsto_diff

   bounded_linear.LIMSEQ ~> bounded_linear.tendsto

   bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto

   LIMSEQ_mult ~> tendsto_mult

   LIMSEQ_inverse ~> tendsto_inverse

   LIMSEQ_divide ~> tendsto_divide

   LIMSEQ_pow ~> tendsto_power

   LIMSEQ_setsum ~> tendsto_setsum

   LIMSEQ_setprod ~> tendsto_setprod

   LIMSEQ_norm_zero ~> tendsto_norm_zero_iff

   LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff

   LIMSEQ_imp_rabs ~> tendsto_rabs

   LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]

   LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]

   LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]

   LIMSEQ_Complex ~> tendsto_Complex

   LIM_ident ~> tendsto_ident_at

   LIM_const ~> tendsto_const

   LIM_add ~> tendsto_add

   LIM_add_zero ~> tendsto_add_zero

   LIM_minus ~> tendsto_minus

   LIM_diff ~> tendsto_diff

   LIM_norm ~> tendsto_norm

   LIM_norm_zero ~> tendsto_norm_zero

   LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel

   LIM_norm_zero_iff ~> tendsto_norm_zero_iff

   LIM_rabs ~> tendsto_rabs

   LIM_rabs_zero ~> tendsto_rabs_zero

   LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel

   LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff

   LIM_compose ~> tendsto_compose

   LIM_mult ~> tendsto_mult

   LIM_scaleR ~> tendsto_scaleR

   LIM_of_real ~> tendsto_of_real

   LIM_power ~> tendsto_power

   LIM_inverse ~> tendsto_inverse

   LIM_sgn ~> tendsto_sgn

   isCont_LIM_compose ~> isCont_tendsto_compose

   bounded_linear.LIM ~> bounded_linear.tendsto

   bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero

   bounded_bilinear.LIM ~> bounded_bilinear.tendsto

   bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero

   bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero

   bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero

   LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]

 * Theory Complex_Main: The definition of infinite series was

 generalized.  Now it is defined on the type class {topological_space,

 comm_monoid_add}.  Hence it is useable also for extended real numbers.

 * Theory Complex_Main: The complex exponential function "expi" is now

 a type-constrained abbreviation for "exp :: complex => complex"; thus

 several polymorphic lemmas about "exp" are now applicable to "expi".

 * Code generation:

   - Theory Library/Code_Char_ord provides native ordering of

     characters in the target language.

   - Commands code_module and code_library are legacy, use export_code

     instead.

   - Method "evaluation" is legacy, use method "eval" instead.

   - Legacy evaluator "SML" is deactivated by default.  May be

     reactivated by the following theory command:

       setup {* Value.add_evaluator ("SML", Codegen.eval_term) *}

 * Declare ext [intro] by default.  Rare INCOMPATIBILITY.

 * New proof method "induction" that gives induction hypotheses the

 name "IH", thus distinguishing them from further hypotheses that come

 from rule induction.  The latter are still called "hyps".  Method

 "induction" is a thin wrapper around "induct" and follows the same

 syntax.

 * Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is

 still available as a legacy feature for some time.

 * Nitpick:

   - Added "need" and "total_consts" options.

   - Reintroduced "show_skolems" option by popular demand.

   - Renamed attribute: nitpick_def ~> nitpick_unfold.

     INCOMPATIBILITY.

 * Sledgehammer:

   - Use quasi-sound (and efficient) translations by default.

   - Added support for the following provers: E-ToFoF, LEO-II,

     Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax.

   - Automatically preplay and minimize proofs before showing them if

     this can be done within reasonable time.

   - sledgehammer available_provers ~> sledgehammer supported_provers.

     INCOMPATIBILITY.

   - Added "preplay_timeout", "slicing", "type_enc", "sound",

     "max_mono_iters", and "max_new_mono_instances" options.

   - Removed "explicit_apply" and "full_types" options as well as "Full

     Types" Proof General menu item. INCOMPATIBILITY.

 * Metis:

   - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.

   - Obsoleted "metisFT" -- use "metis (full_types)" instead.

     INCOMPATIBILITY.

 * Command 'try':

   - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and

     "elim:" options. INCOMPATIBILITY.

   - Introduced 'try' that not only runs 'try_methods' but also

     'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'.

 * Quickcheck:

   - Added "eval" option to evaluate terms for the found counterexample

     (currently only supported by the default (exhaustive) tester).

   - Added post-processing of terms to obtain readable counterexamples

     (currently only supported by the default (exhaustive) tester).

   - New counterexample generator quickcheck[narrowing] enables

     narrowing-based testing.  Requires the Glasgow Haskell compiler

     with its installation location defined in the Isabelle settings

     environment as ISABELLE_GHC.

   - Removed quickcheck tester "SML" based on the SML code generator

     (formly in HOL/Library).

 * Function package: discontinued option "tailrec".  INCOMPATIBILITY,

 use 'partial_function' instead.

 * Theory Library/Extended_Reals replaces now the positive extended

 reals found in probability theory. This file is extended by

 Multivariate_Analysis/Extended_Real_Limits.

 * Theory Library/Old_Recdef: old 'recdef' package has been moved here,

 from where it must be imported explicitly if it is really required.

 INCOMPATIBILITY.

 * Theory Library/Wfrec: well-founded recursion combinator "wfrec" has

 been moved here.  INCOMPATIBILITY.

 * Theory Library/Saturated provides type of numbers with saturated

 arithmetic.

 * Theory Library/Product_Lattice defines a pointwise ordering for the

 product type 'a * 'b, and provides instance proofs for various order

 and lattice type classes.

 * Theory Library/Countable now provides the "countable_datatype" proof

 method for proving "countable" class instances for datatypes.

 * Theory Library/Cset_Monad allows do notation for computable sets

 (cset) via the generic monad ad-hoc overloading facility.

 * Library: Theories of common data structures are split into theories

 for implementation, an invariant-ensuring type, and connection to an

 abstract type. INCOMPATIBILITY.

   - RBT is split into RBT and RBT_Mapping.

   - AssocList is split and renamed into AList and AList_Mapping.

   - DList is split into DList_Impl, DList, and DList_Cset.

   - Cset is split into Cset and List_Cset.

 * Theory Library/Nat_Infinity has been renamed to

 Library/Extended_Nat, with name changes of the following types and

 constants:

   type inat   ~> type enat

   Fin         ~> enat

   Infty       ~> infinity (overloaded)

   iSuc        ~> eSuc

   the_Fin     ~> the_enat

 Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has

 been renamed accordingly. INCOMPATIBILITY.

 * Session Multivariate_Analysis: The euclidean_space type class now

 fixes a constant "Basis :: 'a set" consisting of the standard

 orthonormal basis for the type. Users now have the option of

 quantifying over this set instead of using the "basis" function, e.g.

 "ALL x:Basis. P x" vs "ALL i<DIM('a). P (basis i)".

 * Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed

 to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants

 "Cart_nth" and "Cart_lambda" have been respectively renamed to

 "vec_nth" and "vec_lambda"; theorems mentioning those names have

 changed to match. Definition theorems for overloaded constants now use

 the standard "foo_vec_def" naming scheme. A few other theorems have

 been renamed as follows (INCOMPATIBILITY):

   Cart_eq          ~> vec_eq_iff

   dist_nth_le_cart ~> dist_vec_nth_le

   tendsto_vector   ~> vec_tendstoI

   Cauchy_vector    ~> vec_CauchyI

 * Session Multivariate_Analysis: Several duplicate theorems have been

 removed, and other theorems have been renamed or replaced with more

 general versions. INCOMPATIBILITY.

   finite_choice ~> finite_set_choice

   eventually_conjI ~> eventually_conj

   eventually_and ~> eventually_conj_iff

   eventually_false ~> eventually_False

   setsum_norm ~> norm_setsum

   Lim_sequentially ~> LIMSEQ_def

   Lim_ident_at ~> LIM_ident

   Lim_const ~> tendsto_const

   Lim_cmul ~> tendsto_scaleR [OF tendsto_const]

   Lim_neg ~> tendsto_minus

   Lim_add ~> tendsto_add

   Lim_sub ~> tendsto_diff

   Lim_mul ~> tendsto_scaleR

   Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]

   Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]

   Lim_linear ~> bounded_linear.tendsto

   Lim_component ~> tendsto_euclidean_component

   Lim_component_cart ~> tendsto_vec_nth

   Lim_inner ~> tendsto_inner [OF tendsto_const]

   dot_lsum ~> inner_setsum_left

   dot_rsum ~> inner_setsum_right

   continuous_cmul ~> continuous_scaleR [OF continuous_const]

   continuous_neg ~> continuous_minus

   continuous_sub ~> continuous_diff

   continuous_vmul ~> continuous_scaleR [OF _ continuous_const]

   continuous_mul ~> continuous_scaleR

   continuous_inv ~> continuous_inverse

   continuous_at_within_inv ~> continuous_at_within_inverse

   continuous_at_inv ~> continuous_at_inverse

   continuous_at_norm ~> continuous_norm [OF continuous_at_id]

   continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id]

   continuous_at_component ~> continuous_component [OF continuous_at_id]

   continuous_on_neg ~> continuous_on_minus

   continuous_on_sub ~> continuous_on_diff

   continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const]

   continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const]

   continuous_on_mul ~> continuous_on_scaleR

   continuous_on_mul_real ~> continuous_on_mult

   continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]

   continuous_on_norm ~> continuous_on_norm [OF continuous_on_id]

   continuous_on_inverse ~> continuous_on_inv

   uniformly_continuous_on_neg ~> uniformly_continuous_on_minus

   uniformly_continuous_on_sub ~> uniformly_continuous_on_diff

   subset_interior ~> interior_mono

   subset_closure ~> closure_mono

   closure_univ ~> closure_UNIV

   real_arch_lt ~> reals_Archimedean2

   real_arch ~> reals_Archimedean3

   real_abs_norm ~> abs_norm_cancel

   real_abs_sub_norm ~> norm_triangle_ineq3

   norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2

 * Session HOL-Probability:

   - Caratheodory's extension lemma is now proved for ring_of_sets.

   - Infinite products of probability measures are now available.

   - Sigma closure is independent, if the generator is independent

   - Use extended reals instead of positive extended

     reals. INCOMPATIBILITY.

 * Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY.

   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

   monofun_fun_fun ~> fun_belowD

   monofun_fun_arg ~> monofunE

   monofun_lub_fun ~> adm_monofun [THEN admD]

   cont_lub_fun ~> adm_cont [THEN admD]

   cont2cont_Rep_CFun ~> cont2cont_APP

   cont_Rep_CFun_app ~> cont_APP_app

   cont_Rep_CFun_app_app ~> cont_APP_app_app

   cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE]

   cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE]

   contlub_cfun ~> lub_APP [symmetric]

   contlub_LAM ~> lub_LAM [symmetric]

   thelubI ~> lub_eqI

   UU_I ~> bottomI

   lift_distinct1 ~> lift.distinct(1)

   lift_distinct2 ~> lift.distinct(2)

   Def_not_UU ~> lift.distinct(2)

   Def_inject ~> lift.inject

   below_UU_iff ~> below_bottom_iff

   eq_UU_iff ~> eq_bottom_iff

 *** Document preparation ***

 * Antiquotation @{rail} layouts railroad syntax diagrams, see also

 isar-ref manual, both for description and actual application of the

 same.

 * Antiquotation @{value} evaluates the given term and presents its

 result.