Isabelle NEWS -- history of user-relevant changes

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

 (Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.)

 New in this Isabelle version

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

 *** General ***

 * Toplevel theorem statements have been simplified as follows:

   theorems             ~>  lemmas

   schematic_lemma      ~>  schematic_goal

   schematic_theorem    ~>  schematic_goal

   schematic_corollary  ~>  schematic_goal

 Command-line tool "isabelle update_theorems" updates theory sources

 accordingly.

 * Toplevel theorem statement 'proposition' is another alias for

 'theorem'.

 * HTML presentation uses the standard IsabelleText font and Unicode

 rendering of Isabelle symbols like Isabelle/Scala/jEdit.  The former

 print mode "HTML" looses its special meaning.

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

 * Improved scheduling for urgent print tasks (e.g. command state output,

 interactive queries) wrt. long-running background tasks.

 * IDE support for the source-level debugger of Poly/ML, to work with

 Isabelle/ML and official Standard ML. Configuration option "ML_debugger"

 and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',

 'SML_file_no_debug' control compilation of sources with debugging

 information. The Debugger panel allows to set breakpoints (via context

 menu), step through stopped threads, evaluate local ML expressions etc.

 At least one Debugger view needs to be active to have any effect on the

 running ML program.

 * The main Isabelle executable is managed as single-instance Desktop

 application uniformly on all platforms: Linux, Windows, Mac OS X.

 * The text overview column (status of errors, warnings etc.) is updated

 asynchronously, leading to much better editor reactivity. Moreover, the

 full document node content is taken into account.

 * The State panel manages explicit proof state output, with jEdit action

 "isabelle.update-state" (shortcut S+ENTER) to trigger update according

 to cursor position. Option "editor_output_state" controls implicit proof

 state output in the Output panel: suppressing this reduces resource

 requirements of prover time and GUI space.

 *** Document preparation ***

 * Isabelle control symbols for markup and formatting:

   \<^smallskip>   \smallskip

   \<^medskip>   \medskip

   \<^bigskip>   \bigskip

   \<^item>  \item  (itemize)

   \<^enum>  \item  (enumeration)

 *** Isar ***

 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the

 proof body as well, abstracted over relevant parameters.

 * Improved type-inference for theorem statement 'obtains': separate

 parameter scope for of each clause.

 * Term abbreviations via 'is' patterns also work for schematic

 statements: result is abstracted over unknowns.

 * Local goals ('have', 'show', 'hence', 'thus') allow structured

 statements like fixes/assumes/shows in theorem specifications, but the

 notation is postfix with keywords 'if' (or 'when') and 'for'. For

 example:

   have result: "C x y"

     if "A x" and "B y"

     for x :: 'a and y :: 'a

     <proof>

 The local assumptions are bound to the name "that". The result is

 exported from context of the statement as usual. The above roughly

 corresponds to a raw proof block like this:

   {

     fix x :: 'a and y :: 'a

     assume that: "A x" "B y"

     have "C x y" <proof>

   }

   note result = this

 The keyword 'when' may be used instead of 'if', to indicate 'presume'

 instead of 'assume' above.

 * The meaning of 'show' with Pure rule statements has changed: premises

 are treated in the sense of 'assume', instead of 'presume'. This means,

 a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows:

   show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

 or:

   show "C x" if "A x" "B x" for x

 Rare INCOMPATIBILITY, the old behaviour may be recovered as follows:

   show "C x" when "A x" "B x" for x

 * New command 'supply' supports fact definitions during goal refinement

 ('apply' scripts).

 * New command 'consider' states rules for generalized elimination and

 case splitting. This is like a toplevel statement "theorem obtains" used

 within a proof body; or like a multi-branch 'obtain' without activation

 of the local context elements yet.

 * Proof method "cases" allows to specify the rule as first entry of

 chained facts.  This is particularly useful with 'consider':

   consider (a) A | (b) B | (c) C <proof>

   then have something

   proof cases

     case a

     then show ?thesis <proof>

   next

     case b

     then show ?thesis <proof>

   next

     case c

     then show ?thesis <proof>

   qed

 * Command 'case' allows fact name and attribute specification like this:

   case a: (c xs)

   case a [attributes]: (c xs)

 Facts that are introduced by invoking the case context are uniformly

 qualified by "a"; the same name is used for the cumulative fact. The old

 form "case (c xs) [attributes]" is no longer supported. Rare

 INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,

 and always put attributes in front.

 * The standard proof method of commands 'proof' and '..' is now called

 "standard" to make semantically clear what it is; the old name "default"

 is still available as legacy for some time. Documentation now explains

 '..' more accurately as "by standard" instead of "by rule".

 * Command 'subgoal' allows to impose some structure on backward

 refinements, to avoid proof scripts degenerating into long of 'apply'

 sequences. Further explanations and examples are given in the isar-ref

 manual.

 * Proof method "goal_cases" turns the current subgoals into cases within

 the context; the conclusion is bound to variable ?case in each case. For

 example:

 lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

   and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"

 proof goal_cases

   case (1 x)

   then show ?case using \<open>A x\<close> \<open>B x\<close> sorry

 next

   case (2 y z)

   then show ?case using \<open>U y\<close> \<open>V z\<close> sorry

 qed

 lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

   and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"

 proof goal_cases

   case prems: 1

   then show ?case using prems sorry

 next

   case prems: 2

   then show ?case using prems sorry

 qed

 * The undocumented feature of implicit cases goal1, goal2, goal3, etc.

 is marked as legacy, and will be removed eventually. The proof method

 "goals" achieves a similar effect within regular Isar; often it can be

 done more adequately by other means (e.g. 'consider').

 * Nesting of Isar goal structure has been clarified: the context after

 the initial backwards refinement is retained for the whole proof, within

 all its context sections (as indicated via 'next'). This is e.g.

 relevant for 'using', 'including', 'supply':

   have "A \<and> A" if a: A for A

     supply [simp] = a

   proof

     show A by simp

   next

     show A by simp

   qed

 * Method "sleep" succeeds after a real-time delay (in seconds). This is

 occasionally useful for demonstration and testing purposes.

 *** Pure ***

 * Command 'print_definitions' prints dependencies of definitional

 specifications. This functionality used to be part of 'print_theory'.

 * The vacuous fact "TERM x" may be established "by fact" or as `TERM x`

 as well, not just "by this" or "." as before.

 * Configuration option rule_insts_schematic has been discontinued

 (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.

 * Abbreviations in type classes now carry proper sort constraint.

 Rare INCOMPATIBILITY in situations where the previous misbehaviour

 has been exploited.

 * Refinement of user-space type system in type classes: pseudo-local

 operations behave more similar to abbreviations.  Potential

 INCOMPATIBILITY in exotic situations.

 *** HOL ***

 * Combinator to represent case distinction on products is named "case_prod",

 uniformly, discontinuing any input aliasses.  Very popular theorem aliasses

 have been retained.

 Consolidated facts:

   PairE ~> prod.exhaust

   Pair_eq ~> prod.inject

   pair_collapse ~> prod.collapse

   Pair_fst_snd_eq ~> prod_eq_iff

   split_twice ~> prod.case_distrib

   split_weak_cong ~> prod.case_cong_weak

   split_split ~> prod.split

   split_split_asm ~> prod.split_asm

   splitI ~> case_prodI

   splitD ~> case_prodD

   splitI2 ~> case_prodI2

   splitI2' ~> case_prodI2'

   splitE ~> case_prodE

   splitE' ~> case_prodE'

   split_pair ~> case_prod_Pair

   split_eta ~> case_prod_eta

   split_comp ~> case_prod_comp

   mem_splitI ~> mem_case_prodI

   mem_splitI2 ~> mem_case_prodI2

   mem_splitE ~> mem_case_prodE

   The_split ~> The_case_prod

   cond_split_eta ~> cond_case_prod_eta

   Collect_split_in_rel_leE ~> Collect_case_prod_in_rel_leE

   Collect_split_in_rel_leI ~> Collect_case_prod_in_rel_leI

   in_rel_Collect_split_eq ~> in_rel_Collect_case_prod_eq

   Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD

   Collect_split_Grp_inD ~> Collect_case_prod_Grp_in

   Domain_Collect_split ~> Domain_Collect_case_prod

   Image_Collect_split ~> Image_Collect_case_prod

   Range_Collect_split ~> Range_Collect_case_prod

   Eps_split ~> Eps_case_prod

   Eps_split_eq ~> Eps_case_prod_eq

   split_rsp ~> case_prod_rsp

   curry_split ~> curry_case_prod

   split_curry ~> case_prod_curry

 Changes in structure HOLogic:

   split_const ~> case_prod_const

   mk_split ~> mk_case_prod

   mk_psplits ~> mk_ptupleabs

   strip_psplits ~> strip_ptupleabs

 INCOMPATIBILITY.

 * Commands 'inductive' and 'inductive_set' work better when names for

 intro rules are omitted: the "cases" and "induct" rules no longer

 declare empty case_names, but no case_names at all. This allows to use

 numbered cases in proofs, without requiring method "goal_cases".

 * The 'typedef' command has been upgraded from a partially checked

 "axiomatization", to a full definitional specification that takes the

 global collection of overloaded constant / type definitions into

 account. Type definitions with open dependencies on overloaded

 definitions need to be specified as "typedef (overloaded)". This

 provides extra robustness in theory construction. Rare INCOMPATIBILITY.

 * Qualification of various formal entities in the libraries is done more

 uniformly via "context begin qualified definition ... end" instead of

 old-style "hide_const (open) ...". Consequently, both the defined

 constant and its defining fact become qualified, e.g. Option.is_none and

 Option.is_none_def. Occasional INCOMPATIBILITY in applications.

 * Some old and rarely used ASCII replacement syntax has been removed.

 INCOMPATIBILITY, standard syntax with symbols should be used instead.

 The subsequent commands help to reproduce the old forms, e.g. to

 simplify porting old theories:

   type_notation Map.map  (infixr "~=>" 0)

   notation Map.map_comp  (infixl "o'_m" 55)

   type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21)

   notation FuncSet.funcset  (infixr "->" 60)

   notation FuncSet.extensional_funcset  (infixr "->\<^sub>E" 60)

   notation Omega_Words_Fun.conc (infixr "conc" 65)

   notation Preorder.equiv ("op ~~")

     and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)

 * The alternative notation "\<Colon>" for type and sort constraints has been

 removed: in LaTeX document output it looks the same as "::".

 INCOMPATIBILITY, use plain "::" instead.

 * Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has

 been removed. INCOMPATIBILITY.

 * Quickcheck setup for finite sets.

 * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.

 * Sledgehammer:

   - The MaSh relevance filter has been sped up.

   - Proof reconstruction has been improved, to minimize the incidence of

     cases where Sledgehammer gives a proof that does not work.

   - Auto Sledgehammer now minimizes and preplays the results.

   - Handle Vampire 4.0 proof output without raising exception.

   - Eliminated "MASH" environment variable. Use the "MaSh" option in

     Isabelle/jEdit instead. INCOMPATIBILITY.

   - Eliminated obsolete "blocking" option and related subcommands.

 * Nitpick:

   - Fixed soundness bug in translation of "finite" predicate.

   - Fixed soundness bug in "destroy_constrs" optimization.

   - Removed "check_potential" and "check_genuine" options.

   - Eliminated obsolete "blocking" option.

 * New (co)datatype package:

   - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF

     structure on the raw type to an abstract type defined using typedef.

   - Always generate "case_transfer" theorem.

 * Transfer:

   - new methods for interactive debugging of 'transfer' and 

     'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',

     'transfer_prover_start' and 'transfer_prover_end'.

 * Division on integers is bootstrapped directly from division on

 naturals and uses generic numeral algorithm for computations.

 Slight INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes

 former simprocs binary_int_div and binary_int_mod

 * Tightened specification of class semiring_no_zero_divisors.  Slight

 INCOMPATIBILITY.

 * Class algebraic_semidom introduces common algebraic notions of

 integral (semi)domains, particularly units.  Although

 logically subsumed by fields, is is not a super class of these

 in order not to burden fields with notions that are trivial there.

 * Class normalization_semidom specifies canonical representants

 for equivalence classes of associated elements in an integral

 (semi)domain.  This formalizes associated elements as well.

 * Abstract specification of gcd/lcm operations in classes semiring_gcd,

 semiring_Gcd, semiring_Lcd.  Minor INCOMPATIBILITY: facts gcd_nat.commute

 and gcd_int.commute are subsumed by gcd.commute, as well as gcd_nat.assoc

 and gcd_int.assoc by gcd.assoc.

 * Former constants Fields.divide (_ / _) and Divides.div (_ div _)

 are logically unified to Rings.divide in syntactic type class

 Rings.divide, with infix syntax (_ div _).  Infix syntax (_ / _)

 for field division is added later as abbreviation in class Fields.inverse.

 INCOMPATIBILITY,  instantiations must refer to Rings.divide rather

 than the former separate constants, hence infix syntax (_ / _) is usually

 not available during instantiation.

 * Library/Multiset:

   - Renamed multiset inclusion operators:

       < ~> <#

       \<subset> ~> \<subset>#

       <= ~> <=#

       \<le> ~> \<le>#

       \<subseteq> ~> \<subseteq>#

     INCOMPATIBILITY.

   - "'a multiset" is no longer an instance of the "order",

     "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",

     "semilattice_inf", and "semilattice_sup" type classes. The theorems

     previously provided by these type classes (directly or indirectly)

     are now available through the "subset_mset" interpretation

     (e.g. add_mono ~> subset_mset.add_mono).

     INCOMPATIBILITY.

   - Renamed conversions:

       multiset_of ~> mset

       multiset_of_set ~> mset_set

       set_of ~> set_mset

     INCOMPATIBILITY

   - Renamed lemmas:

       mset_le_def ~> subseteq_mset_def

       mset_less_def ~> subset_mset_def

       less_eq_multiset.rep_eq ~> subseteq_mset_def

     INCOMPATIBILITY

   - Removed lemmas generated by lift_definition:

     less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer

     less_eq_multiset_def

     INCOMPATIBILITY

 * Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals and Cauchy's integral theorem,

     ported from HOL Light

 * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'

 command. Minor INCOMPATIBILITY, use 'function' instead.

 * Recursive function definitions ('fun', 'function', 'partial_function')

 no longer expose the low-level "_def" facts of the internal

 construction. INCOMPATIBILITY, enable option "function_defs" in the

 context for rare situations where these facts are really needed.

 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed.

 * Library/Omega_Words_Fun: Infinite words modeled as functions nat => 'a.

 *** ML ***

 * The auxiliary module Pure/display.ML has been eliminated. Its

 elementary thm print operations are now in Pure/more_thm.ML and thus

 called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.

 * Simproc programming interfaces have been simplified:

 Simplifier.make_simproc and Simplifier.define_simproc supersede various

 forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that

 term patterns for the left-hand sides are specified with implicitly

 fixed variables, like top-level theorem statements. INCOMPATIBILITY.

 * Instantiation rules have been re-organized as follows:

   Thm.instantiate  (*low-level instantiation with named arguments*)

   Thm.instantiate' (*version with positional arguments*)

   Drule.infer_instantiate  (*instantiation with type inference*)

   Drule.infer_instantiate'  (*version with positional arguments*)

 The LHS only requires variable specifications, instead of full terms.

 Old cterm_instantiate is superseded by infer_instantiate.

 INCOMPATIBILITY, need to re-adjust some ML names and types accordingly.

 * Old tactic shorthands atac, rtac, etac, dtac, ftac have been

 discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.

 instead (with proper context).

 * Thm.instantiate (and derivatives) no longer require the LHS of the

 instantiation to be certified: plain variables are given directly.

 * Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous

 quasi-bound variables (like the Simplifier), instead of accidentally

 named local fixes. This has the potential to improve stability of proof

 tools, but can also cause INCOMPATIBILITY for tools that don't observe

 the proof context discipline.

 *** System ***

 * Property values in etc/symbols may contain spaces, if written with the

 replacement character "␣" (Unicode point 0x2324).  For example:

   \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono

 * Command-line tool "isabelle jedit_client" allows to connect to already

 running Isabelle/jEdit process. This achieves the effect of

 single-instance applications seen on common GUI desktops.

 * Command-line tool "isabelle update_then" expands old Isar command

 conflations:

     hence  ~>  then have

     thus   ~>  then show

 This syntax is more orthogonal and improves readability and

 maintainability of proofs.

 * Poly/ML default platform architecture may be changed from 32bit to

 64bit via system option ML_system_64. A system restart (and rebuild)

 is required after change.

 * Poly/ML 5.5.3 runs natively on x86-windows and x86_64-windows,

 which both allow larger heap space than former x86-cygwin.

 * Java runtime environment for x86_64-windows allows to use larger heap

 space.

 * Java runtime options are determined separately for 32bit vs. 64bit

 platforms as follows.

   - Isabelle desktop application: platform-specific files that are

     associated with the main app bundle

   - isabelle jedit: settings

     JEDIT_JAVA_SYSTEM_OPTIONS

     JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64

   - isabelle build: settings

     ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64

 * Bash shell function "jvmpath" has been renamed to "platform_path": it

 is relevant both for Poly/ML and JVM processes.

 New in Isabelle2015 (May 2015)

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

 *** General ***

 * Local theory specification commands may have a 'private' or

 'qualified' modifier to restrict name space accesses to the local scope,

 as provided by some "context begin ... end" block. For example:

   context

   begin

   private definition ...

   private lemma ...

   qualified definition ...

   qualified lemma ...

   lemma ...

   theorem ...

   end

 * Command 'experiment' opens an anonymous locale context with private

 naming policy.

 * Command 'notepad' requires proper nesting of begin/end and its proof

 structure in the body: 'oops' is no longer supported here. Minor

 INCOMPATIBILITY, use 'sorry' instead.

 * Command 'named_theorems' declares a dynamic fact within the context,

 together with an attribute to maintain the content incrementally. This

 supersedes functor Named_Thms in Isabelle/ML, but with a subtle change

 of semantics due to external visual order vs. internal reverse order.

 * 'find_theorems': search patterns which are abstractions are

 schematically expanded before search. Search results match the naive

 expectation more closely, particularly wrt. abbreviations.

 INCOMPATIBILITY.

 * Commands 'method_setup' and 'attribute_setup' now work within a local

 theory context.

 * Outer syntax commands are managed authentically within the theory

 context, without implicit global state. Potential for accidental

 INCOMPATIBILITY, make sure that required theories are really imported.

 * Historical command-line terminator ";" is no longer accepted (and

 already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle

 update_semicolons" to remove obsolete semicolons from old theory

 sources.

 * Structural composition of proof methods (meth1; meth2) in Isar

 corresponds to (tac1 THEN_ALL_NEW tac2) in ML.

 * The Eisbach proof method language allows to define new proof methods

 by combining existing ones with their usual syntax. The "match" proof

 method provides basic fact/term matching in addition to

 premise/conclusion matching through Subgoal.focus, and binds fact names

 from matches as well as term patterns within matches. The Isabelle

 documentation provides an entry "eisbach" for the Eisbach User Manual.

 Sources and various examples are in ~~/src/HOL/Eisbach/.

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

 * Improved folding mode "isabelle" based on Isar syntax. Alternatively,

 the "sidekick" mode may be used for document structure.

 * Extended bracket matching based on Isar language structure. System

 option jedit_structure_limit determines maximum number of lines to scan

 in the buffer.

 * Support for BibTeX files: context menu, context-sensitive token

 marker, SideKick parser.

 * Document antiquotation @{cite} provides formal markup, which is

 interpreted semi-formally based on .bib files that happen to be open in

 the editor (hyperlinks, completion etc.).

 * Less waste of vertical space via negative line spacing (see Global

 Options / Text Area).

 * Improved graphview panel with optional output of PNG or PDF, for

 display of 'thy_deps', 'class_deps' etc.

 * The commands 'thy_deps' and 'class_deps' allow optional bounds to

 restrict the visualized hierarchy.

 * Improved scheduling for asynchronous print commands (e.g. provers

 managed by the Sledgehammer panel) wrt. ongoing document processing.

 *** Document preparation ***

 * Document markup commands 'chapter', 'section', 'subsection',

 'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any

 context, even before the initial 'theory' command. Obsolete proof

 commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been

 discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw'

 instead. The old 'header' command is still retained for some time, but

 should be replaced by 'chapter', 'section' etc. (using "isabelle

 update_header"). Minor INCOMPATIBILITY.

 * Official support for "tt" style variants, via \isatt{...} or

 \begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or

 verbatim environment of LaTeX is no longer used. This allows @{ML} etc.

 as argument to other macros (such as footnotes).

 * Document antiquotation @{verbatim} prints ASCII text literally in "tt"

 style.

 * Discontinued obsolete option "document_graph": session_graph.pdf is

 produced unconditionally for HTML browser_info and PDF-LaTeX document.

 * Diagnostic commands and document markup commands within a proof do not

 affect the command tag for output. Thus commands like 'thm' are subject

 to proof document structure, and no longer "stick out" accidentally.

 Commands 'text' and 'txt' merely differ in the LaTeX style, not their

 tags. Potential INCOMPATIBILITY in exotic situations.

 * System option "pretty_margin" is superseded by "thy_output_margin",

 which is also accessible via document antiquotation option "margin".

 Only the margin for document output may be changed, but not the global

 pretty printing: that is 76 for plain console output, and adapted

 dynamically in GUI front-ends. Implementations of document

 antiquotations need to observe the margin explicitly according to

 Thy_Output.string_of_margin. Minor INCOMPATIBILITY.

 * Specification of 'document_files' in the session ROOT file is

 mandatory for document preparation. The legacy mode with implicit

 copying of the document/ directory is no longer supported. Minor

 INCOMPATIBILITY.

 *** Pure ***

 * Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"

 etc.) allow an optional context of local variables ('for' declaration):

 these variables become schematic in the instantiated theorem; this

 behaviour is analogous to 'for' in attributes "where" and "of".

 Configuration option rule_insts_schematic (default false) controls use

 of schematic variables outside the context. Minor INCOMPATIBILITY,

 declare rule_insts_schematic = true temporarily and update to use local

 variable declarations or dummy patterns instead.

 * Explicit instantiation via attributes "where", "of", and proof methods

 "rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns

 ("_") that stand for anonymous local variables.

 * Generated schematic variables in standard format of exported facts are

 incremented to avoid material in the proof context. Rare

 INCOMPATIBILITY, explicit instantiation sometimes needs to refer to

 different index.

 * Lexical separation of signed and unsigned numerals: categories "num"

 and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence

 of numeral signs, particularly in expressions involving infix syntax

 like "(- 1) ^ n".

 * Old inner token category "xnum" has been discontinued.  Potential

 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num"

 token category instead.

 *** HOL ***

 * New (co)datatype package:

   - The 'datatype_new' command has been renamed 'datatype'. The old

     command of that name is now called 'old_datatype' and is provided

     by "~~/src/HOL/Library/Old_Datatype.thy". See

     'isabelle doc datatypes' for information on porting.

     INCOMPATIBILITY.

   - Renamed theorems:

       disc_corec ~> corec_disc

       disc_corec_iff ~> corec_disc_iff

       disc_exclude ~> distinct_disc

       disc_exhaust ~> exhaust_disc

       disc_map_iff ~> map_disc_iff

       sel_corec ~> corec_sel

       sel_exhaust ~> exhaust_sel

       sel_map ~> map_sel

       sel_set ~> set_sel

       sel_split ~> split_sel

       sel_split_asm ~> split_sel_asm

       strong_coinduct ~> coinduct_strong

       weak_case_cong ~> case_cong_weak

     INCOMPATIBILITY.

   - The "no_code" option to "free_constructors", "datatype_new", and

     "codatatype" has been renamed "plugins del: code".

     INCOMPATIBILITY.

   - The rules "set_empty" have been removed. They are easy

     consequences of other set rules "by auto".

     INCOMPATIBILITY.

   - The rule "set_cases" is now registered with the "[cases set]"

     attribute. This can influence the behavior of the "cases" proof

     method when more than one case rule is applicable (e.g., an

     assumption is of the form "w : set ws" and the method "cases w"

     is invoked). The solution is to specify the case rule explicitly

     (e.g. "cases w rule: widget.exhaust").

     INCOMPATIBILITY.

   - Renamed theories:

       BNF_Comp ~> BNF_Composition

       BNF_FP_Base ~> BNF_Fixpoint_Base

       BNF_GFP ~> BNF_Greatest_Fixpoint

       BNF_LFP ~> BNF_Least_Fixpoint

       BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions

       Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions

     INCOMPATIBILITY.

   - Lifting and Transfer setup for basic HOL types sum and prod (also

     option) is now performed by the BNF package. Theories Lifting_Sum,

     Lifting_Product and Lifting_Option from Main became obsolete and

     were removed. Changed definitions of the relators rel_prod and

     rel_sum (using inductive).

     INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead

     of rel_prod_def and rel_sum_def.

     Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names

     changed (e.g. map_prod_transfer ~> prod.map_transfer).

   - Parametricity theorems for map functions, relators, set functions,

     constructors, case combinators, discriminators, selectors and

     (co)recursors are automatically proved and registered as transfer

     rules.

 * Old datatype package:

   - The old 'datatype' command has been renamed 'old_datatype', and

     'rep_datatype' has been renamed 'old_rep_datatype'. They are

     provided by "~~/src/HOL/Library/Old_Datatype.thy". See

     'isabelle doc datatypes' for information on porting.

     INCOMPATIBILITY.

   - Renamed theorems:

       weak_case_cong ~> case_cong_weak

     INCOMPATIBILITY.

   - Renamed theory:

       ~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy

     INCOMPATIBILITY.

 * Nitpick:

   - Fixed soundness bug related to the strict and non-strict subset

     operations.

 * Sledgehammer:

   - CVC4 is now included with Isabelle instead of CVC3 and run by

     default.

   - Z3 is now always enabled by default, now that it is fully open

     source. The "z3_non_commercial" option is discontinued.

   - Minimization is now always enabled by default.

     Removed sub-command:

       min

   - Proof reconstruction, both one-liners and Isar, has been

     dramatically improved.

   - Improved support for CVC4 and veriT.

 * Old and new SMT modules:

   - The old 'smt' method has been renamed 'old_smt' and moved to

     'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility,

     until applications have been ported to use the new 'smt' method. For

     the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must

     be installed, and the environment variable "OLD_Z3_SOLVER" must

     point to it.

     INCOMPATIBILITY.

   - The 'smt2' method has been renamed 'smt'.

     INCOMPATIBILITY.

   - New option 'smt_reconstruction_step_timeout' to limit the

     reconstruction time of Z3 proof steps in the new 'smt' method.

   - New option 'smt_statistics' to display statistics of the new 'smt'

     method, especially runtime statistics of Z3 proof reconstruction.

 * Lifting: command 'lift_definition' allows to execute lifted constants

 that have as a return type a datatype containing a subtype. This

 overcomes long-time limitations in the area of code generation and

 lifting, and avoids tedious workarounds.

 * Command and antiquotation "value" provide different evaluation slots

 (again), where the previous strategy (NBE after ML) serves as default.

 Minor INCOMPATIBILITY.

 * Add NO_MATCH-simproc, allows to check for syntactic non-equality.

 * field_simps: Use NO_MATCH-simproc for distribution rules, to avoid

 non-termination in case of distributing a division. With this change

 field_simps is in some cases slightly less powerful, if it fails try to

 add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY.

 * Separate class no_zero_divisors has been given up in favour of fully

 algebraic semiring_no_zero_divisors. INCOMPATIBILITY.

 * Class linordered_semidom really requires no zero divisors.

 INCOMPATIBILITY.

 * Classes division_ring, field and linordered_field always demand

 "inverse 0 = 0". Given up separate classes division_ring_inverse_zero,

 field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.

 * Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit

 additive inverse operation. INCOMPATIBILITY.

 * Complex powers and square roots. The functions "ln" and "powr" are now

 overloaded for types real and complex, and 0 powr y = 0 by definition.

 INCOMPATIBILITY: type constraints may be necessary.

 * The functions "sin" and "cos" are now defined for any type of sort

 "{real_normed_algebra_1,banach}" type, so in particular on "real" and

 "complex" uniformly. Minor INCOMPATIBILITY: type constraints may be

 needed.

 * New library of properties of the complex transcendental functions sin,

 cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.

 * The factorial function, "fact", now has type "nat => 'a" (of a sort

 that admits numeric types including nat, int, real and complex.

 INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type

 constraint, and the combination "real (fact k)" is likely to be

 unsatisfactory. If a type conversion is still necessary, then use

 "of_nat (fact k)" or "real_of_nat (fact k)".

 * Removed functions "natfloor" and "natceiling", use "nat o floor" and

 "nat o ceiling" instead. A few of the lemmas have been retained and

 adapted: in their names "natfloor"/"natceiling" has been replaced by

 "nat_floor"/"nat_ceiling".

 * Qualified some duplicated fact names required for boostrapping the

 type class hierarchy:

   ab_add_uminus_conv_diff ~> diff_conv_add_uminus

   field_inverse_zero ~> inverse_zero

   field_divide_inverse ~> divide_inverse

   field_inverse ~> left_inverse

 Minor INCOMPATIBILITY.

 * Eliminated fact duplicates:

   mult_less_imp_less_right ~> mult_right_less_imp_less

   mult_less_imp_less_left ~> mult_left_less_imp_less

 Minor INCOMPATIBILITY.

 * Fact consolidation: even_less_0_iff is subsumed by

 double_add_less_zero_iff_single_add_less_zero (simp by default anyway).

 * Generalized and consolidated some theorems concerning divsibility:

   dvd_reduce ~> dvd_add_triv_right_iff

   dvd_plus_eq_right ~> dvd_add_right_iff

   dvd_plus_eq_left ~> dvd_add_left_iff

 Minor INCOMPATIBILITY.

 * "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"

 and part of theory Main.

   even_def ~> even_iff_mod_2_eq_zero

 INCOMPATIBILITY.

 * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor

 INCOMPATIBILITY.

 * Bootstrap of listsum as special case of abstract product over lists.

 Fact rename:

     listsum_def ~> listsum.eq_foldr

 INCOMPATIBILITY.

 * Product over lists via constant "listprod".

 * Theory List: renamed drop_Suc_conv_tl and nth_drop' to

 Cons_nth_drop_Suc.

 * New infrastructure for compiling, running, evaluating and testing

 generated code in target languages in HOL/Library/Code_Test. See

 HOL/Codegenerator_Test/Code_Test* for examples.

 * Library/Multiset:

   - Introduced "replicate_mset" operation.

   - Introduced alternative characterizations of the multiset ordering in

     "Library/Multiset_Order".

   - Renamed multiset ordering:

       <# ~> #<#

       <=# ~> #<=#

       \<subset># ~> #\<subset>#

       \<subseteq># ~> #\<subseteq>#

     INCOMPATIBILITY.

   - Introduced abbreviations for ill-named multiset operations:

       <#, \<subset># abbreviate < (strict subset)

       <=#, \<le>#, \<subseteq># abbreviate <= (subset or equal)

     INCOMPATIBILITY.

   - Renamed

       in_multiset_of ~> in_multiset_in_set

       Multiset.fold ~> fold_mset

       Multiset.filter ~> filter_mset

     INCOMPATIBILITY.

   - Removed mcard, is equal to size.

   - Added attributes:

       image_mset.id [simp]

       image_mset_id [simp]

       elem_multiset_of_set [simp, intro]

       comp_fun_commute_plus_mset [simp]

       comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp]

       in_mset_fold_plus_iff [iff]

       set_of_Union_mset [simp]

       in_Union_mset_iff [iff]

     INCOMPATIBILITY.

 * Library/Sum_of_Squares: simplified and improved "sos" method. Always

 use local CSDP executable, which is much faster than the NEOS server.

 The "sos_cert" functionality is invoked as "sos" with additional

 argument. Minor INCOMPATIBILITY.

 * HOL-Decision_Procs: New counterexample generator quickcheck

 [approximation] for inequalities of transcendental functions. Uses

 hardware floating point arithmetic to randomly discover potential

 counterexamples. Counterexamples are certified with the "approximation"

 method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for

 examples.

 * HOL-Probability: Reworked measurability prover

   - applies destructor rules repeatedly

   - removed application splitting (replaced by destructor rule)

   - added congruence rules to rewrite measure spaces under the sets

     projection

 * New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for

 single-step rewriting with subterm selection based on patterns.

 *** ML ***

 * Subtle change of name space policy: undeclared entries are now

 considered inaccessible, instead of accessible via the fully-qualified

 internal name. This mainly affects Name_Space.intern (and derivatives),

 which may produce an unexpected Long_Name.hidden prefix. Note that

 contemporary applications use the strict Name_Space.check (and

 derivatives) instead, which is not affected by the change. Potential

 INCOMPATIBILITY in rare applications of Name_Space.intern.

 * Subtle change of error semantics of Toplevel.proof_of: regular user

 ERROR instead of internal Toplevel.UNDEF.

 * Basic combinators map, fold, fold_map, split_list, apply are available

 as parameterized antiquotations, e.g. @{map 4} for lists of quadruples.

 * Renamed "pairself" to "apply2", in accordance to @{apply 2}.

 INCOMPATIBILITY.

 * Former combinators NAMED_CRITICAL and CRITICAL for central critical

 sections have been discontinued, in favour of the more elementary

 Multithreading.synchronized and its high-level derivative

 Synchronized.var (which is usually sufficient in applications). Subtle

 INCOMPATIBILITY: synchronized access needs to be atomic and cannot be

 nested.

 * Synchronized.value (ML) is actually synchronized (as in Scala): subtle

 change of semantics with minimal potential for INCOMPATIBILITY.

 * The main operations to certify logical entities are Thm.ctyp_of and

 Thm.cterm_of with a local context; old-style global theory variants are

 available as Thm.global_ctyp_of and Thm.global_cterm_of.

 INCOMPATIBILITY.

 * Elementary operations in module Thm are no longer pervasive.

 INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of,

 Thm.term_of etc.

 * Proper context for various elementary tactics: assume_tac,

 resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac,

 compose_tac, Splitter.split_tac etc. INCOMPATIBILITY.

 * Tactical PARALLEL_ALLGOALS is the most common way to refer to

 PARALLEL_GOALS.

 * Goal.prove_multi is superseded by the fully general Goal.prove_common,

 which also allows to specify a fork priority.

 * Antiquotation @{command_spec "COMMAND"} is superseded by

 @{command_keyword COMMAND} (usually without quotes and with PIDE

 markup). Minor INCOMPATIBILITY.

 * Cartouches within ML sources are turned into values of type

 Input.source (with formal position information).

 *** System ***

 * The Isabelle tool "update_cartouches" changes theory files to use

 cartouches instead of old-style {* verbatim *} or `alt_string` tokens.

 * The Isabelle tool "build" provides new options -X, -k, -x.

 * Discontinued old-fashioned "codegen" tool. Code generation can always

 be externally triggered using an appropriate ROOT file plus a

 corresponding theory. Parametrization is possible using environment

 variables, or ML snippets in the most extreme cases. Minor

 INCOMPATIBILITY.

 * JVM system property "isabelle.threads" determines size of Scala thread

 pool, like Isabelle system option "threads" for ML.

 * JVM system property "isabelle.laf" determines the default Swing

 look-and-feel, via internal class name or symbolic name as in the jEdit

 menu Global Options / Appearance.

 * Support for Proof General and Isar TTY loop has been discontinued.

 Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.

 New in Isabelle2014 (August 2014)

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

 *** General ***

 * Support for official Standard ML within the Isabelle context.

 Command 'SML_file' reads and evaluates the given Standard ML file.

 Toplevel bindings are stored within the theory context; the initial

 environment is restricted to the Standard ML implementation of

 Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'

 and 'SML_export' allow to exchange toplevel bindings between the two

 separate environments.  See also ~~/src/Tools/SML/Examples.thy for

 some examples.

 * Standard tactics and proof methods such as "clarsimp", "auto" and

 "safe" now preserve equality hypotheses "x = expr" where x is a free

 variable.  Locale assumptions and chained facts containing "x"

 continue to be useful.  The new method "hypsubst_thin" and the

 configuration option "hypsubst_thin" (within the attribute name space)

 restore the previous behavior.  INCOMPATIBILITY, especially where

 induction is done after these methods or when the names of free and

 bound variables clash.  As first approximation, old proofs may be

 repaired by "using [[hypsubst_thin = true]]" in the critical spot.

 * More static checking of proof methods, which allows the system to

 form a closure over the concrete syntax.  Method arguments should be

 processed in the original proof context as far as possible, before

 operating on the goal state.  In any case, the standard discipline for

 subgoal-addressing needs to be observed: no subgoals or a subgoal

 number that is out of range produces an empty result sequence, not an

 exception.  Potential INCOMPATIBILITY for non-conformant tactical

 proof tools.

 * Lexical syntax (inner and outer) supports text cartouches with

 arbitrary nesting, and without escapes of quotes etc.  The Prover IDE

 supports input via ` (backquote).

 * The outer syntax categories "text" (for formal comments and document

 markup commands) and "altstring" (for literal fact references) allow

 cartouches as well, in addition to the traditional mix of quotations.

 * Syntax of document antiquotation @{rail} now uses \<newline> instead

 of "\\", to avoid the optical illusion of escaped backslash within

 string token.  General renovation of its syntax using text cartouches.

 Minor INCOMPATIBILITY.

 * Discontinued legacy_isub_isup, which was a temporary workaround for

 Isabelle/ML in Isabelle2013-1.  The prover process no longer accepts

 old identifier syntax with \<^isub> or \<^isup>.  Potential

 INCOMPATIBILITY.

 * Document antiquotation @{url} produces markup for the given URL,

 which results in an active hyperlink within the text.

 * Document antiquotation @{file_unchecked} is like @{file}, but does

 not check existence within the file-system.

 * Updated and extended manuals: codegen, datatypes, implementation,

 isar-ref, jedit, system.

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

 * Improved Document panel: simplified interaction where every single

 mouse click (re)opens document via desktop environment or as jEdit

 buffer.

 * Support for Navigator plugin (with toolbar buttons), with connection

 to PIDE hyperlinks.

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

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

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

 auxiliary ML files.

 * Improved syntactic and semantic completion mechanism, with simple

 templates, completion language context, name-space completion,

 file-name completion, spell-checker completion.

 * Refined GUI popup for completion: more robust key/mouse event

 handling and propagation to enclosing text area -- avoid loosing

 keystrokes with slow / remote graphics displays.

 * Completion popup supports both ENTER and TAB (default) to select an

 item, depending on Isabelle options.

 * Refined insertion of completion items wrt. jEdit text: multiple

 selections, rectangular selections, rectangular selection as "tall

 caret".

 * Integrated spell-checker for document text, comments etc. with

 completion popup and context-menu.

 * More general "Query" panel supersedes "Find" panel, with GUI access

 to commands 'find_theorems' and 'find_consts', as well as print

 operations for the context.  Minor incompatibility in keyboard

 shortcuts etc.: replace action isabelle-find by isabelle-query.

 * Search field for all output panels ("Output", "Query", "Info" etc.)

 to highlight text via regular expression.

 * Option "jedit_print_mode" (see also "Plugin Options / Isabelle /

 General") allows to specify additional print modes for the prover

 process, without requiring old-fashioned command-line invocation of

 "isabelle jedit -m MODE".

 * More support for remote files (e.g. http) using standard Java

 networking operations instead of jEdit virtual file-systems.

 * Empty editors buffers that are no longer required (e.g.\ via theory

 imports) are automatically removed from the document model.

 * Improved monitor panel.

 * Improved Console/Scala plugin: more uniform scala.Console output,

 more robust treatment of threads and interrupts.

 * Improved management of dockable windows: clarified keyboard focus

 and window placement wrt. main editor view; optional menu item to

 "Detach" a copy where this makes sense.

 * New Simplifier Trace panel provides an interactive view of the

 simplification process, enabled by the "simp_trace_new" attribute

 within the context.

 *** Pure ***

 * Low-level type-class commands 'classes', 'classrel', 'arities' have

 been discontinued to avoid the danger of non-trivial axiomatization

 that is not immediately visible.  INCOMPATIBILITY, use regular

 'instance' command with proof.  The required OFCLASS(...) theorem

 might be postulated via 'axiomatization' beforehand, or the proof

 finished trivially if the underlying class definition is made vacuous

 (without any assumptions).  See also Isabelle/ML operations

 Axclass.class_axiomatization, Axclass.classrel_axiomatization,

 Axclass.arity_axiomatization.

 * Basic constants of Pure use more conventional names and are always

 qualified.  Rare INCOMPATIBILITY, but with potentially serious

 consequences, notably for tools in Isabelle/ML.  The following

 renaming needs to be applied:

   ==             ~>  Pure.eq

   ==>            ~>  Pure.imp

   all            ~>  Pure.all

   TYPE           ~>  Pure.type

   dummy_pattern  ~>  Pure.dummy_pattern

 Systematic porting works by using the following theory setup on a

 *previous* Isabelle version to introduce the new name accesses for the

 old constants:

 setup {*

   fn thy => thy

     |> Sign.root_path

     |> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="

     |> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"

     |> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"

     |> Sign.restore_naming thy

 *}

 Thus ML antiquotations like @{const_name Pure.eq} may be used already.

 Later the application is moved to the current Isabelle version, and

 the auxiliary aliases are deleted.

 * Attributes "where" and "of" allow an optional context of local

 variables ('for' declaration): these variables become schematic in the

 instantiated theorem.

 * Obsolete attribute "standard" has been discontinued (legacy since

 Isabelle2012).  Potential INCOMPATIBILITY, use explicit 'for' context

 where instantiations with schematic variables are intended (for

 declaration commands like 'lemmas' or attributes like "of").  The

 following temporary definition may help to port old applications:

   attribute_setup standard =

     "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"

 * More thorough check of proof context for goal statements and

 attributed fact expressions (concerning background theory, declared

 hyps).  Potential INCOMPATIBILITY, tools need to observe standard

 context discipline.  See also Assumption.add_assumes and the more

 primitive Thm.assume_hyps.

 * Inner syntax token language allows regular quoted strings "..."

 (only makes sense in practice, if outer syntax is delimited

 differently, e.g. via cartouches).

 * Command 'print_term_bindings' supersedes 'print_binds' for clarity,

 but the latter is retained some time as Proof General legacy.

 * Code generator preprocessor: explicit control of simp tracing on a

 per-constant basis.  See attribute "code_preproc".

 *** HOL ***

 * Code generator: enforce case of identifiers only for strict target

 language requirements.  INCOMPATIBILITY.

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

 INCOMPATIBILITY.

 * Code generator: minimize exported identifiers by default.  Minor

 INCOMPATIBILITY.

 * Code generation for SML and OCaml: dropped arcane "no_signatures"

 option.  Minor INCOMPATIBILITY.

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

 INCOMPATIBILITY.

 * "declare [[code drop: ...]]" drops all code equations associated

 with the given constants.

 * Code generations are provided for make, fields, extend and truncate

 operations on records.

 * Command and antiquotation "value" are now hardcoded against nbe and

 ML.  Minor INCOMPATIBILITY.

 * Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY.

 * The symbol "\<newline>" may be used within char or string literals

 to represent (Char Nibble0 NibbleA), i.e. ASCII newline.

 * Qualified String.implode and String.explode.  INCOMPATIBILITY.

 * Simplifier: Enhanced solver of preconditions of rewrite rules can

 now deal with conjunctions.  For help with converting proofs, the old

 behaviour of the simplifier can be restored like this: declare/using

 [[simp_legacy_precond]].  This configuration option will disappear

 again in the future.  INCOMPATIBILITY.

 * Simproc "finite_Collect" is no longer enabled by default, due to

 spurious crashes and other surprises.  Potential INCOMPATIBILITY.

 * Moved new (co)datatype package and its dependencies from session

   "HOL-BNF" to "HOL".  The commands 'bnf', 'wrap_free_constructors',

   'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now

   part of theory "Main".

   Theory renamings:

     FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)

     Library/Wfrec.thy ~> Wfrec.thy

     Library/Zorn.thy ~> Zorn.thy

     Cardinals/Order_Relation.thy ~> Order_Relation.thy

     Library/Order_Union.thy ~> Cardinals/Order_Union.thy

     Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy

     Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy

     Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy

     Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy

     Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy

     BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy

     BNF/Basic_BNFs.thy ~> Basic_BNFs.thy

     BNF/BNF_Comp.thy ~> BNF_Comp.thy

     BNF/BNF_Def.thy ~> BNF_Def.thy

     BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy

     BNF/BNF_GFP.thy ~> BNF_GFP.thy

     BNF/BNF_LFP.thy ~> BNF_LFP.thy

     BNF/BNF_Util.thy ~> BNF_Util.thy

     BNF/Coinduction.thy ~> Coinduction.thy

     BNF/More_BNFs.thy ~> Library/More_BNFs.thy

     BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy

     BNF/Examples/* ~> BNF_Examples/*

   New theories:

     Wellorder_Extension.thy (split from Zorn.thy)

     Library/Cardinal_Notations.thy

     Library/BNF_Axomatization.thy

     BNF_Examples/Misc_Primcorec.thy

     BNF_Examples/Stream_Processor.thy

   Discontinued theories:

     BNF/BNF.thy

     BNF/Equiv_Relations_More.thy

 INCOMPATIBILITY.

 * New (co)datatype package:

   - Command 'primcorec' is fully implemented.

   - Command 'datatype_new' generates size functions ("size_xxx" and

     "size") as required by 'fun'.

   - BNFs are integrated with the Lifting tool and new-style

     (co)datatypes with Transfer.

   - Renamed commands:

       datatype_new_compat ~> datatype_compat

       primrec_new ~> primrec

       wrap_free_constructors ~> free_constructors

     INCOMPATIBILITY.

   - The generated constants "xxx_case" and "xxx_rec" have been renamed

     "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").

     INCOMPATIBILITY.

   - The constant "xxx_(un)fold" and related theorems are no longer

     generated.  Use "xxx_(co)rec" or define "xxx_(un)fold" manually

     using "prim(co)rec".

     INCOMPATIBILITY.

   - No discriminators are generated for nullary constructors by

     default, eliminating the need for the odd "=:" syntax.

     INCOMPATIBILITY.

   - No discriminators or selectors are generated by default by

     "datatype_new", unless custom names are specified or the new

     "discs_sels" option is passed.

     INCOMPATIBILITY.

 * Old datatype package:

   - The generated theorems "xxx.cases" and "xxx.recs" have been

     renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" ->

     "sum.case").  INCOMPATIBILITY.

   - The generated constants "xxx_case", "xxx_rec", and "xxx_size" have

     been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g.,

     "prod_case" ~> "case_prod").  INCOMPATIBILITY.

 * The types "'a list" and "'a option", their set and map functions,

   their relators, and their selectors are now produced using the new

   BNF-based datatype package.

   Renamed constants:

     Option.set ~> set_option

     Option.map ~> map_option

     option_rel ~> rel_option

   Renamed theorems:

     set_def ~> set_rec[abs_def]

     map_def ~> map_rec[abs_def]

     Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")

     option.recs ~> option.rec

     list_all2_def ~> list_all2_iff

     set.simps ~> set_simps (or the slightly different "list.set")

     map.simps ~> list.map

     hd.simps ~> list.sel(1)

     tl.simps ~> list.sel(2-3)

     the.simps ~> option.sel

 INCOMPATIBILITY.

 * The following map functions and relators have been renamed:

     sum_map ~> map_sum

     map_pair ~> map_prod

     prod_rel ~> rel_prod

     sum_rel ~> rel_sum

     fun_rel ~> rel_fun

     set_rel ~> rel_set

     filter_rel ~> rel_filter

     fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy")

     cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy")

     vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy")

 INCOMPATIBILITY.

 * Lifting and Transfer:

   - a type variable as a raw type is supported

   - stronger reflexivity prover

   - rep_eq is always generated by lift_definition

   - setup for Lifting/Transfer is now automated for BNFs

     + holds for BNFs that do not contain a dead variable

     + relator_eq, relator_mono, relator_distr, relator_domain,

       relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total,

       right_unique, right_total, left_unique, left_total are proved

       automatically

     + definition of a predicator is generated automatically

     + simplification rules for a predicator definition are proved

       automatically for datatypes

   - consolidation of the setup of Lifting/Transfer

     + property that a relator preservers reflexivity is not needed any

       more

       Minor INCOMPATIBILITY.

     + left_total and left_unique rules are now transfer rules

       (reflexivity_rule attribute not needed anymore)

       INCOMPATIBILITY.

     + Domainp does not have to be a separate assumption in

       relator_domain theorems (=> more natural statement)

       INCOMPATIBILITY.

   - registration of code equations is more robust

     Potential INCOMPATIBILITY.

   - respectfulness proof obligation is preprocessed to a more readable

     form

     Potential INCOMPATIBILITY.

   - eq_onp is always unfolded in respectfulness proof obligation

     Potential INCOMPATIBILITY.

   - unregister lifting setup for Code_Numeral.integer and

     Code_Numeral.natural

     Potential INCOMPATIBILITY.

   - Lifting.invariant -> eq_onp

     INCOMPATIBILITY.

 * New internal SAT solver "cdclite" that produces models and proof

 traces.  This solver replaces the internal SAT solvers "enumerate" and

 "dpll".  Applications that explicitly used one of these two SAT

 solvers should use "cdclite" instead. In addition, "cdclite" is now

 the default SAT solver for the "sat" and "satx" proof methods and

 corresponding tactics; the old default can be restored using "declare

 [[sat_solver = zchaff_with_proofs]]".  Minor INCOMPATIBILITY.

 * SMT module: A new version of the SMT module, temporarily called

 "SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g.,

 4.3). The new proof method is called "smt2". CVC3 and CVC4 are also

 supported as oracles. Yices is no longer supported, because no version

 of the solver can handle both SMT-LIB 2 and quantifiers.

 * Activation of Z3 now works via "z3_non_commercial" system option

 (without requiring restart), instead of former settings variable

 "Z3_NON_COMMERCIAL".  The option can be edited in Isabelle/jEdit menu

 Plugin Options / Isabelle / General.

 * Sledgehammer:

   - Z3 can now produce Isar proofs.

   - MaSh overhaul:

     . New SML-based learning algorithms eliminate the dependency on

       Python and increase performance and reliability.

     . MaSh and MeSh are now used by default together with the

       traditional MePo (Meng-Paulson) relevance filter. To disable

       MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin

       Options / Isabelle / General to "none".

   - New option:

       smt_proofs

   - Renamed options:

       isar_compress ~> compress

       isar_try0 ~> try0

 INCOMPATIBILITY.

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

 * Nitpick:

   - Fixed soundness bug whereby mutually recursive datatypes could

     take infinite values.

   - Fixed soundness bug with low-level number functions such as

     "Abs_Integ" and "Rep_Integ".

   - Removed "std" option.

   - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to

     "hide_types".

 * Metis: Removed legacy proof method 'metisFT'. Use 'metis

 (full_types)' instead. INCOMPATIBILITY.

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

 * Adjustion of INF and SUP operations:

   - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.

   - Consolidated theorem names containing INFI and SUPR: have INF and

     SUP instead uniformly.

   - More aggressive normalization of expressions involving INF and Inf

     or SUP and Sup.

   - INF_image and SUP_image do not unfold composition.

   - Dropped facts INF_comp, SUP_comp.

   - Default congruence rules strong_INF_cong and strong_SUP_cong, with

     simplifier implication in premises.  Generalize and replace former

     INT_cong, SUP_cong

 INCOMPATIBILITY.

 * SUP and INF generalized to conditionally_complete_lattice.

 * Swapped orientation of facts image_comp and vimage_comp:

   image_compose ~> image_comp [symmetric]

   image_comp ~> image_comp [symmetric]

   vimage_compose ~> vimage_comp [symmetric]

   vimage_comp ~> vimage_comp [symmetric]

 INCOMPATIBILITY.

 * Theory reorganization: split of Big_Operators.thy into

 Groups_Big.thy and Lattices_Big.thy.

 * Consolidated some facts about big group operators:

     setsum_0' ~> setsum.neutral

     setsum_0 ~> setsum.neutral_const

     setsum_addf ~> setsum.distrib

     setsum_cartesian_product ~> setsum.cartesian_product

     setsum_cases ~> setsum.If_cases

     setsum_commute ~> setsum.commute

     setsum_cong ~> setsum.cong

     setsum_delta ~> setsum.delta

     setsum_delta' ~> setsum.delta'

     setsum_diff1' ~> setsum.remove

     setsum_empty ~> setsum.empty

     setsum_infinite ~> setsum.infinite

     setsum_insert ~> setsum.insert

     setsum_inter_restrict'' ~> setsum.inter_filter

     setsum_mono_zero_cong_left ~> setsum.mono_neutral_cong_left

     setsum_mono_zero_cong_right ~> setsum.mono_neutral_cong_right

     setsum_mono_zero_left ~> setsum.mono_neutral_left

     setsum_mono_zero_right ~> setsum.mono_neutral_right

     setsum_reindex ~> setsum.reindex

     setsum_reindex_cong ~> setsum.reindex_cong

     setsum_reindex_nonzero ~> setsum.reindex_nontrivial

     setsum_restrict_set ~> setsum.inter_restrict

     setsum_Plus ~> setsum.Plus

     setsum_setsum_restrict ~> setsum.commute_restrict

     setsum_Sigma ~> setsum.Sigma

     setsum_subset_diff ~> setsum.subset_diff

     setsum_Un_disjoint ~> setsum.union_disjoint

     setsum_UN_disjoint ~> setsum.UNION_disjoint

     setsum_Un_Int ~> setsum.union_inter

     setsum_Union_disjoint ~> setsum.Union_disjoint

     setsum_UNION_zero ~> setsum.Union_comp

     setsum_Un_zero ~> setsum.union_inter_neutral

     strong_setprod_cong ~> setprod.strong_cong

     strong_setsum_cong ~> setsum.strong_cong

     setprod_1' ~> setprod.neutral

     setprod_1 ~> setprod.neutral_const

     setprod_cartesian_product ~> setprod.cartesian_product

     setprod_cong ~> setprod.cong

     setprod_delta ~> setprod.delta

     setprod_delta' ~> setprod.delta'

     setprod_empty ~> setprod.empty

     setprod_infinite ~> setprod.infinite

     setprod_insert ~> setprod.insert

     setprod_mono_one_cong_left ~> setprod.mono_neutral_cong_left

     setprod_mono_one_cong_right ~> setprod.mono_neutral_cong_right

     setprod_mono_one_left ~> setprod.mono_neutral_left

     setprod_mono_one_right ~> setprod.mono_neutral_right

     setprod_reindex ~> setprod.reindex

     setprod_reindex_cong ~> setprod.reindex_cong

     setprod_reindex_nonzero ~> setprod.reindex_nontrivial

     setprod_Sigma ~> setprod.Sigma

     setprod_subset_diff ~> setprod.subset_diff

     setprod_timesf ~> setprod.distrib

     setprod_Un2 ~> setprod.union_diff2

     setprod_Un_disjoint ~> setprod.union_disjoint

     setprod_UN_disjoint ~> setprod.UNION_disjoint

     setprod_Un_Int ~> setprod.union_inter

     setprod_Union_disjoint ~> setprod.Union_disjoint

     setprod_Un_one ~> setprod.union_inter_neutral

   Dropped setsum_cong2 (simple variant of setsum.cong).

   Dropped setsum_inter_restrict' (simple variant of setsum.inter_restrict)

   Dropped setsum_reindex_id, setprod_reindex_id

     (simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]).

 INCOMPATIBILITY.

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

   Fact consolidations:

     min_max.inf_assoc ~> min.assoc

     min_max.inf_commute ~> min.commute

     min_max.inf_left_commute ~> min.left_commute

     min_max.inf_idem ~> min.idem

     min_max.inf_left_idem ~> min.left_idem

     min_max.inf_right_idem ~> min.right_idem

     min_max.sup_assoc ~> max.assoc

     min_max.sup_commute ~> max.commute

     min_max.sup_left_commute ~> max.left_commute

     min_max.sup_idem ~> max.idem

     min_max.sup_left_idem ~> max.left_idem

     min_max.sup_inf_distrib1 ~> max_min_distrib2

     min_max.sup_inf_distrib2 ~> max_min_distrib1

     min_max.inf_sup_distrib1 ~> min_max_distrib2

     min_max.inf_sup_distrib2 ~> min_max_distrib1

     min_max.distrib ~> min_max_distribs

     min_max.inf_absorb1 ~> min.absorb1

     min_max.inf_absorb2 ~> min.absorb2

     min_max.sup_absorb1 ~> max.absorb1

     min_max.sup_absorb2 ~> max.absorb2

     min_max.le_iff_inf ~> min.absorb_iff1

     min_max.le_iff_sup ~> max.absorb_iff2

     min_max.inf_le1 ~> min.cobounded1

     min_max.inf_le2 ~> min.cobounded2

     le_maxI1, min_max.sup_ge1 ~> max.cobounded1

     le_maxI2, min_max.sup_ge2 ~> max.cobounded2

     min_max.le_infI1 ~> min.coboundedI1

     min_max.le_infI2 ~> min.coboundedI2

     min_max.le_supI1 ~> max.coboundedI1

     min_max.le_supI2 ~> max.coboundedI2

     min_max.less_infI1 ~> min.strict_coboundedI1

     min_max.less_infI2 ~> min.strict_coboundedI2

     min_max.less_supI1 ~> max.strict_coboundedI1

     min_max.less_supI2 ~> max.strict_coboundedI2

     min_max.inf_mono ~> min.mono

     min_max.sup_mono ~> max.mono

     min_max.le_infI, min_max.inf_greatest ~> min.boundedI

     min_max.le_supI, min_max.sup_least ~> max.boundedI

     min_max.le_inf_iff ~> min.bounded_iff

     min_max.le_sup_iff ~> max.bounded_iff

 For min_max.inf_sup_aci, prefer (one of) min.commute, min.assoc,

 min.left_commute, min.left_idem, max.commute, max.assoc,

 max.left_commute, max.left_idem directly.

 For min_max.inf_sup_ord, prefer (one of) min.cobounded1,

 min.cobounded2, max.cobounded1m max.cobounded2 directly.

 For min_ac or max_ac, prefer more general collection ac_simps.

 INCOMPATIBILITY.

 * Theorem disambiguation Inf_le_Sup (on finite sets) ~>

 Inf_fin_le_Sup_fin.  INCOMPATIBILITY.

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

 INCOMPATIBILITY.

 * Fact generalization and consolidation:

     neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1

 INCOMPATIBILITY.

 * Purely algebraic definition of even.  Fact generalization and

   consolidation:

     nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd

     even_zero_(nat|int) ~> even_zero

 INCOMPATIBILITY.

 * Abolished neg_numeral.

   - Canonical representation for minus one is "- 1".

   - Canonical representation for other negative numbers is "- (numeral _)".

   - When devising rule sets for number calculation, consider the

     following canonical cases: 0, 1, numeral _, - 1, - numeral _.

   - HOLogic.dest_number also recognizes numerals in non-canonical forms

     like "numeral One", "- numeral One", "- 0" and even "- ... - _".

   - Syntax for negative numerals is mere input syntax.

 INCOMPATIBILITY.

 * Reduced name variants for rules on associativity and commutativity:

     add_assoc ~> add.assoc

     add_commute ~> add.commute

     add_left_commute ~> add.left_commute

     mult_assoc ~> mult.assoc

     mult_commute ~> mult.commute

     mult_left_commute ~> mult.left_commute

     nat_add_assoc ~> add.assoc

     nat_add_commute ~> add.commute

     nat_add_left_commute ~> add.left_commute

     nat_mult_assoc ~> mult.assoc

     nat_mult_commute ~> mult.commute

     eq_assoc ~> iff_assoc

     eq_left_commute ~> iff_left_commute

 INCOMPATIBILITY.

 * Fact collections add_ac and mult_ac are considered old-fashioned.

 Prefer ac_simps instead, or specify rules

 (add|mult).(assoc|commute|left_commute) individually.

 * Elimination of fact duplicates:

     equals_zero_I ~> minus_unique

     diff_eq_0_iff_eq ~> right_minus_eq

     nat_infinite ~> infinite_UNIV_nat

     int_infinite ~> infinite_UNIV_int

 INCOMPATIBILITY.

 * Fact name consolidation:

     diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus

     minus_le_self_iff ~> neg_less_eq_nonneg

     le_minus_self_iff ~> less_eq_neg_nonpos

     neg_less_nonneg ~> neg_less_pos

     less_minus_self_iff ~> less_neg_neg [simp]

 INCOMPATIBILITY.

 * More simplification rules on unary and binary minus:

 add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,

 add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,

 add_minus_cancel, diff_add_cancel, le_add_same_cancel1,

 le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,

 minus_add_cancel, uminus_add_conv_diff.  These correspondingly have

 been taken away from fact collections algebra_simps and field_simps.

 INCOMPATIBILITY.

 To restore proofs, the following patterns are helpful:

 a) Arbitrary failing proof not involving "diff_def":

 Consider simplification with algebra_simps or field_simps.

 b) Lifting rules from addition to subtraction:

 Try with "using <rule for addition> of [... "- _" ...]" by simp".

 c) Simplification with "diff_def": just drop "diff_def".

 Consider simplification with algebra_simps or field_simps;

 or the brute way with

 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".

 * Introduce bdd_above and bdd_below in theory

 Conditionally_Complete_Lattices, use them instead of explicitly

 stating boundedness of sets.

 * ccpo.admissible quantifies only over non-empty chains to allow more

 syntax-directed proof rules; the case of the empty chain shows up as

 additional case in fixpoint induction proofs.  INCOMPATIBILITY.

 * Removed and renamed theorems in Series:

   summable_le         ~>  suminf_le

   suminf_le           ~>  suminf_le_const

   series_pos_le       ~>  setsum_le_suminf

   series_pos_less     ~>  setsum_less_suminf

   suminf_ge_zero      ~>  suminf_nonneg

   suminf_gt_zero      ~>  suminf_pos

   suminf_gt_zero_iff  ~>  suminf_pos_iff

   summable_sumr_LIMSEQ_suminf  ~>  summable_LIMSEQ

   suminf_0_le         ~>  suminf_nonneg [rotate]

   pos_summable        ~>  summableI_nonneg_bounded

   ratio_test          ~>  summable_ratio_test

   removed series_zero, replaced by sums_finite

   removed auxiliary lemmas:

     sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,

     half, le_Suc_ex_iff, lemma_realpow_diff_sumr,

     real_setsum_nat_ivl_bounded, summable_le2, ratio_test_lemma2,

     sumr_minus_one_realpow_zerom, sumr_one_lb_realpow_zero,

     summable_convergent_sumr_iff, sumr_diff_mult_const

 INCOMPATIBILITY.

 * Replace (F)DERIV syntax by has_derivative:

   - "(f has_derivative f') (at x within s)" replaces "FDERIV f x : s : f'"

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

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

   - removed constant isDiff

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

     input syntax.

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

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

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

   - removed DERIV_intros, has_derivative_eq_intros

   - introduced derivative_intros and deriative_eq_intros which

     includes now rules for DERIV, has_derivative and

     has_vector_derivative.

   - Other renamings:

     differentiable_def        ~>  real_differentiable_def

     differentiableE           ~>  real_differentiableE

     fderiv_def                ~>  has_derivative_at

     field_fderiv_def          ~>  field_has_derivative_at

     isDiff_der                ~>  differentiable_def

     deriv_fderiv              ~>  has_field_derivative_def

     deriv_def                 ~>  DERIV_def

 INCOMPATIBILITY.

 * Include more theorems in continuous_intros. Remove the

 continuous_on_intros, isCont_intros collections, these facts are now

 in continuous_intros.

 * Theorems about complex numbers are now stated only using Re and Im,

 the Complex constructor is not used anymore. It is possible to use

 primcorec to defined the behaviour of a complex-valued function.

 Removed theorems about the Complex constructor from the simpset, they

 are available as the lemma collection legacy_Complex_simps. This

 especially removes

     i_complex_of_real: "ii * complex_of_real r = Complex 0 r".

 Instead the reverse direction is supported with

     Complex_eq: "Complex a b = a + \<i> * b"

 Moved csqrt from Fundamental_Algebra_Theorem to Complex.

   Renamings:

     Re/Im                  ~>  complex.sel

     complex_Re/Im_zero     ~>  zero_complex.sel

     complex_Re/Im_add      ~>  plus_complex.sel

     complex_Re/Im_minus    ~>  uminus_complex.sel

     complex_Re/Im_diff     ~>  minus_complex.sel

     complex_Re/Im_one      ~>  one_complex.sel

     complex_Re/Im_mult     ~>  times_complex.sel

     complex_Re/Im_inverse  ~>  inverse_complex.sel

     complex_Re/Im_scaleR   ~>  scaleR_complex.sel

     complex_Re/Im_i        ~>  ii.sel

     complex_Re/Im_cnj      ~>  cnj.sel

     Re/Im_cis              ~>  cis.sel

     complex_divide_def   ~>  divide_complex_def

     complex_norm_def     ~>  norm_complex_def

     cmod_def             ~>  norm_complex_de

   Removed theorems:

     complex_zero_def

     complex_add_def

     complex_minus_def

     complex_diff_def

     complex_one_def

     complex_mult_def

     complex_inverse_def

     complex_scaleR_def

 INCOMPATIBILITY.

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

 Conditionally_Complete_Lattices.  INCOMPATIBILITY.

 * HOL-Library: new theory src/HOL/Library/Tree.thy.

 * HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it

 is subsumed by session Kleene_Algebra in AFP.

 * HOL-Library / theory RBT: various constants and facts are hidden;

 lifting setup is unregistered.  INCOMPATIBILITY.

 * HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.

 * HOL-Word: bit representations prefer type bool over type bit.

 INCOMPATIBILITY.

 * HOL-Word:

   - Abandoned fact collection "word_arith_alts", which is a duplicate

     of "word_arith_wis".

   - Dropped first (duplicated) element in fact collections

     "sint_word_ariths", "word_arith_alts", "uint_word_ariths",

     "uint_word_arith_bintrs".

 * HOL-Number_Theory:

   - consolidated the proofs of the binomial theorem

   - the function fib is again of type nat => nat and not overloaded

   - no more references to Old_Number_Theory in the HOL libraries

     (except the AFP)

 INCOMPATIBILITY.

 * HOL-Multivariate_Analysis:

   - Type class ordered_real_vector for ordered vector spaces.

   - New theory Complex_Basic_Analysis defining complex derivatives,

     holomorphic functions, etc., ported from HOL Light's canal.ml.

   - Changed order of ordered_euclidean_space to be compatible with

     pointwise ordering on products. Therefore instance of

     conditionally_complete_lattice and ordered_real_vector.

     INCOMPATIBILITY: use box instead of greaterThanLessThan or

     explicit set-comprehensions with eucl_less for other (half-)open

     intervals.

   - removed dependencies on type class ordered_euclidean_space with

     introduction of "cbox" on euclidean_space

     - renamed theorems:

         interval ~> box

         mem_interval ~> mem_box

         interval_eq_empty ~> box_eq_empty

         interval_ne_empty ~> box_ne_empty

         interval_sing(1) ~> cbox_sing

         interval_sing(2) ~> box_sing

         subset_interval_imp ~> subset_box_imp

         subset_interval ~> subset_box

         open_interval ~> open_box

         closed_interval ~> closed_cbox

         interior_closed_interval ~> interior_cbox

         bounded_closed_interval ~> bounded_cbox

         compact_interval ~> compact_cbox

         bounded_subset_closed_interval_symmetric ~> bounded_subset_cbox_symmetric

         bounded_subset_closed_interval ~> bounded_subset_cbox

         mem_interval_componentwiseI ~> mem_box_componentwiseI

         convex_box ~> convex_prod

         rel_interior_real_interval ~> rel_interior_real_box

         convex_interval ~> convex_box

         convex_hull_eq_real_interval ~> convex_hull_eq_real_cbox

         frechet_derivative_within_closed_interval ~> frechet_derivative_within_cbox

         content_closed_interval' ~> content_cbox'

         elementary_subset_interval ~> elementary_subset_box

         diameter_closed_interval ~> diameter_cbox

         frontier_closed_interval ~> frontier_cbox

         frontier_open_interval ~> frontier_box

         bounded_subset_open_interval_symmetric ~> bounded_subset_box_symmetric

         closure_open_interval ~> closure_box

         open_closed_interval_convex ~> open_cbox_convex

         open_interval_midpoint ~> box_midpoint

         content_image_affinity_interval ~> content_image_affinity_cbox

         is_interval_interval ~> is_interval_cbox + is_interval_box + is_interval_closed_interval

         bounded_interval ~> bounded_closed_interval + bounded_boxes

     - respective theorems for intervals over the reals:

         content_closed_interval + content_cbox

         has_integral + has_integral_real

         fine_division_exists + fine_division_exists_real

         has_integral_null + has_integral_null_real

         tagged_division_union_interval + tagged_division_union_interval_real

         has_integral_const + has_integral_const_real

         integral_const + integral_const_real

         has_integral_bound + has_integral_bound_real

         integrable_continuous + integrable_continuous_real

         integrable_subinterval + integrable_subinterval_real

         has_integral_reflect_lemma + has_integral_reflect_lemma_real

         integrable_reflect + integrable_reflect_real

         integral_reflect + integral_reflect_real

         image_affinity_interval + image_affinity_cbox

         image_smult_interval + image_smult_cbox

         integrable_const + integrable_const_ivl

         integrable_on_subinterval + integrable_on_subcbox

   - renamed theorems:

     derivative_linear         ~>  has_derivative_bounded_linear

     derivative_is_linear      ~>  has_derivative_linear

     bounded_linear_imp_linear ~>  bounded_linear.linear

 * HOL-Probability:

   - Renamed positive_integral to nn_integral:

     . Renamed all lemmas "*positive_integral*" to *nn_integral*"

       positive_integral_positive ~> nn_integral_nonneg

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

   - replaced the Lebesgue integral on real numbers by the more general

     Bochner integral for functions into a real-normed vector space.

     integral_zero               ~>  integral_zero / integrable_zero

     integral_minus              ~>  integral_minus / integrable_minus

     integral_add                ~>  integral_add / integrable_add

     integral_diff               ~>  integral_diff / integrable_diff

     integral_setsum             ~>  integral_setsum / integrable_setsum

     integral_multc              ~>  integral_mult_left / integrable_mult_left

     integral_cmult              ~>  integral_mult_right / integrable_mult_right

     integral_triangle_inequality~>  integral_norm_bound

     integrable_nonneg           ~>  integrableI_nonneg

     integral_positive           ~>  integral_nonneg_AE

     integrable_abs_iff          ~>  integrable_abs_cancel

     positive_integral_lim_INF   ~>  nn_integral_liminf

     lebesgue_real_affine        ~>  lborel_real_affine

     borel_integral_has_integral ~>  has_integral_lebesgue_integral

     integral_indicator          ~>

          integral_real_indicator / integrable_real_indicator

     positive_integral_fst       ~>  nn_integral_fst'

     positive_integral_fst_measurable ~> nn_integral_fst

     positive_integral_snd_measurable ~> nn_integral_snd

     integrable_fst_measurable   ~>

          integral_fst / integrable_fst / AE_integrable_fst

     integrable_snd_measurable   ~>

          integral_snd / integrable_snd / AE_integrable_snd

     integral_monotone_convergence  ~>

          integral_monotone_convergence / integrable_monotone_convergence

     integral_monotone_convergence_at_top  ~>

          integral_monotone_convergence_at_top /

          integrable_monotone_convergence_at_top

     has_integral_iff_positive_integral_lebesgue  ~>

          has_integral_iff_has_bochner_integral_lebesgue_nonneg

     lebesgue_integral_has_integral  ~>

          has_integral_integrable_lebesgue_nonneg

     positive_integral_lebesgue_has_integral  ~>

          integral_has_integral_lebesgue_nonneg /

          integrable_has_integral_lebesgue_nonneg

     lebesgue_integral_real_affine  ~>

          nn_integral_real_affine

     has_integral_iff_positive_integral_lborel  ~>

          integral_has_integral_nonneg / integrable_has_integral_nonneg

     The following theorems where removed:

     lebesgue_integral_nonneg

     lebesgue_integral_uminus

     lebesgue_integral_cmult

     lebesgue_integral_multc

     lebesgue_integral_cmult_nonneg

     integral_cmul_indicator

     integral_real

   - Formalized properties about exponentially, Erlang, and normal

     distributed random variables.

 * HOL-Decision_Procs: Separate command 'approximate' for approximative

 computation in src/HOL/Decision_Procs/Approximation.  Minor

 INCOMPATIBILITY.

 *** Scala ***

 * The signature and semantics of Document.Snapshot.cumulate_markup /

 select_markup have been clarified.  Markup is now traversed in the

 order of reports given by the prover: later markup is usually more

 specific and may override results accumulated so far.  The elements

 guard is mandatory and checked precisely.  Subtle INCOMPATIBILITY.

 * Substantial reworking of internal PIDE protocol communication

 channels.  INCOMPATIBILITY.

 *** ML ***

 * Subtle change of semantics of Thm.eq_thm: theory stamps are not

 compared (according to Thm.thm_ord), but assumed to be covered by the

 current background theory.  Thus equivalent data produced in different

 branches of the theory graph usually coincides (e.g. relevant for

 theory merge).  Note that the softer Thm.eq_thm_prop is often more

 appropriate than Thm.eq_thm.

 * Proper context for basic Simplifier operations: rewrite_rule,

 rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to

 pass runtime Proof.context (and ensure that the simplified entity

 actually belongs to it).

 * Proper context discipline for read_instantiate and instantiate_tac:

 variables that are meant to become schematic need to be given as

 fixed, and are generalized by the explicit context of local variables.

 This corresponds to Isar attributes "where" and "of" with 'for'

 declaration.  INCOMPATIBILITY, also due to potential change of indices

 of schematic variables.

 * Moved ML_Compiler.exn_trace and other operations on exceptions to

 structure Runtime.  Minor INCOMPATIBILITY.

 * Discontinued old Toplevel.debug in favour of system option

 "ML_exception_trace", which may be also declared within the context

 via "declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.

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

 INCOMPATIBILITY.

 * Configuration option "ML_print_depth" controls the pretty-printing

 depth of the ML compiler within the context.  The old print_depth in

 ML is still available as default_print_depth, but rarely used.  Minor

 INCOMPATIBILITY.

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

 * Simplified programming interface to define ML antiquotations, see

 structure ML_Antiquotation.  Minor INCOMPATIBILITY.

 * ML antiquotation @{here} refers to its source position, which is

 occasionally useful for experimentation and diagnostic purposes.

 * ML antiquotation @{path} produces a Path.T value, similarly to

 Path.explode, but with compile-time check against the file-system and

 some PIDE markup.  Note that unlike theory source, ML does not have a

 well-defined master directory, so an absolute symbolic path

 specification is usually required, e.g. "~~/src/HOL".

 * ML antiquotation @{print} inlines a function to print an arbitrary

 ML value, which is occasionally useful for diagnostic or demonstration

 purposes.

 *** System ***

 * Proof General with its traditional helper scripts is now an optional

 Isabelle component, e.g. see ProofGeneral-4.2-2 from the Isabelle

 component repository http://isabelle.in.tum.de/components/.  Note that

 the "system" manual provides general explanations about add-on

 components, especially those that are not bundled with the release.

 * The raw Isabelle process executable has been renamed from

 "isabelle-process" to "isabelle_process", which conforms to common

 shell naming conventions, and allows to define a shell function within

 the Isabelle environment to avoid dynamic path lookup.  Rare

 incompatibility for old tools that do not use the ISABELLE_PROCESS

 settings variable.

 * Former "isabelle tty" has been superseded by "isabelle console",

 with implicit build like "isabelle jedit", and without the mostly

 obsolete Isar TTY loop.

 * Simplified "isabelle display" tool.  Settings variables DVI_VIEWER

 and PDF_VIEWER now refer to the actual programs, not shell

 command-lines.  Discontinued option -c: invocation may be asynchronous

 via desktop environment, without any special precautions.  Potential

 INCOMPATIBILITY with ambitious private settings.

 * Removed obsolete "isabelle unsymbolize".  Note that the usual format

 for email communication is the Unicode rendering of Isabelle symbols,

 as produced by Isabelle/jEdit, for example.

 * Removed obsolete tool "wwwfind". Similar functionality may be

 integrated into Isabelle/jEdit eventually.

 * Improved 'display_drafts' concerning desktop integration and

 repeated invocation in PIDE front-end: re-use single file

 $ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.

 * Session ROOT specifications require explicit 'document_files' for

 robust dependencies on LaTeX sources.  Only these explicitly given

 files are copied to the document output directory, before document

 processing is started.

 * Windows: support for regular TeX installation (e.g. MiKTeX) instead

 of TeX Live from Cygwin.

 New in Isabelle2013-2 (December 2013)

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

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

 * More robust editing of running commands with internal forks,

 e.g. non-terminating 'by' steps.

 * More relaxed Sledgehammer panel: avoid repeated application of query

 after edits surrounding the command location.

 * More status information about commands that are interrupted

 accidentally (via physical event or Poly/ML runtime system signal,

 e.g. out-of-memory).

 *** System ***

 * More robust termination of external processes managed by

 Isabelle/ML: support cancellation of tasks within the range of

 milliseconds, as required for PIDE document editing with automatically

 tried tools (e.g. Sledgehammer).

 * Reactivated Isabelle/Scala kill command for external processes on

 Mac OS X, which was accidentally broken in Isabelle2013-1 due to a

 workaround for some Debian/Ubuntu Linux versions from 2013.

 New in Isabelle2013-1 (November 2013)

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

 *** General ***

 * Discontinued obsolete 'uses' within theory header.  Note that

 commands like 'ML_file' work without separate declaration of file

 dependencies.  Minor INCOMPATIBILITY.

 * Discontinued redundant 'use' command, which was superseded by

 'ML_file' in Isabelle2013.  Minor INCOMPATIBILITY.

 * Simplified subscripts within identifiers, using plain \<^sub>

 instead of the second copy \<^isub> and \<^isup>.  Superscripts are

 only for literal tokens within notation; explicit mixfix annotations

 for consts or fixed variables may be used as fall-back for unusual

 names.  Obsolete \<twosuperior> has been expanded to \<^sup>2 in

 Isabelle/HOL.  INCOMPATIBILITY, use "isabelle update_sub_sup" to

 standardize symbols as a starting point for further manual cleanup.

 The ML reference variable "legacy_isub_isup" may be set as temporary

 workaround, to make the prover accept a subset of the old identifier

 syntax.

 * Document antiquotations: term style "isub" has been renamed to

 "sub".  Minor INCOMPATIBILITY.

 * Uniform management of "quick_and_dirty" as system option (see also

 "isabelle options"), configuration option within the context (see also

 Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor

 INCOMPATIBILITY, need to use more official Isabelle means to access

 quick_and_dirty, instead of historical poking into mutable reference.

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

 INCOMPATIBILITY.

 * Proper diagnostic command 'print_state'.  Old 'pr' (with its

 implicit change of some global references) is retained for now as

 control command, e.g. for ProofGeneral 3.7.x.

 * Discontinued 'print_drafts' command with its old-fashioned PS output

 and Unix command-line print spooling.  Minor INCOMPATIBILITY: use

 'display_drafts' instead and print via the regular document viewer.

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

 eliminated old "ref" manual.

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

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

 Documentation panel.

 * Dockable window "Documentation" provides access to Isabelle

 documentation.

 * Dockable window "Find" provides query operations for formal entities

 (GUI front-end to 'find_theorems' command).

 * Dockable window "Sledgehammer" manages asynchronous / parallel

 sledgehammer runs over existing document sources, independently of

 normal editing and checking process.

 * Dockable window "Timing" provides an overview of relevant command

 timing information, depending on option jedit_timing_threshold.  The

 same timing information is shown in the extended tooltip of the

 command keyword, when hovering the mouse over it while the CONTROL or

 COMMAND modifier is pressed.

 * Improved dockable window "Theories": Continuous checking of proof

 document (visible and required parts) may be controlled explicitly,

 using check box or shortcut "C+e ENTER".  Individual theory nodes may

 be marked explicitly as required and checked in full, using check box

 or shortcut "C+e SPACE".

 * Improved completion mechanism, which is now managed by the

 Isabelle/jEdit plugin instead of SideKick.  Refined table of Isabelle

 symbol abbreviations (see $ISABELLE_HOME/etc/symbols).

 * Standard jEdit keyboard shortcut C+b complete-word is remapped to

 isabelle.complete for explicit completion in Isabelle sources.

 INCOMPATIBILITY wrt. jEdit defaults, may have to invent new shortcuts

 to resolve conflict.

 * Improved support of various "minor modes" for Isabelle NEWS,

 options, session ROOT etc., with completion and SideKick tree view.

 * Strictly monotonic document update, without premature cancellation of

 running transactions that are still needed: avoid reset/restart of

 such command executions while editing.

 * Support for asynchronous print functions, as overlay to existing

 document content.

 * Support for automatic tools in HOL, which try to prove or disprove

 toplevel theorem statements.

 * Action isabelle.reset-font-size resets main text area font size

 according to Isabelle/Scala plugin option "jedit_font_reset_size" (see

 also "Plugin Options / Isabelle / General").  It can be bound to some

 keyboard shortcut by the user (e.g. C+0 and/or C+NUMPAD0).

 * File specifications in jEdit (e.g. file browser) may refer to

 $ISABELLE_HOME and $ISABELLE_HOME_USER on all platforms.  Discontinued

 obsolete $ISABELLE_HOME_WINDOWS variable.

 * Improved support for Linux look-and-feel "GTK+", see also "Utilities

 / Global Options / Appearance".

 * Improved support of native Mac OS X functionality via "MacOSX"

 plugin, which is now enabled by default.

 *** Pure ***

 * Commands 'interpretation' and 'sublocale' are now target-sensitive.

 In particular, 'interpretation' allows for non-persistent

 interpretation within "context ... begin ... end" blocks offering a

 light-weight alternative to 'sublocale'.  See "isar-ref" manual for

 details.

 * Improved locales diagnostic command 'print_dependencies'.

 * Discontinued obsolete 'axioms' command, which has been marked as

 legacy since Isabelle2009-2.  INCOMPATIBILITY, use 'axiomatization'

 instead, while observing its uniform scope for polymorphism.

 * Discontinued empty name bindings in 'axiomatization'.

 INCOMPATIBILITY.

 * System option "proofs" has been discontinued.  Instead the global

 state of Proofterm.proofs is persistently compiled into logic images

 as required, notably HOL-Proofs.  Users no longer need to change

 Proofterm.proofs dynamically.  Minor INCOMPATIBILITY.

 * Syntax translation functions (print_translation etc.) always depend

 on Proof.context.  Discontinued former "(advanced)" option -- this is

 now the default.  Minor INCOMPATIBILITY.

 * Former global reference trace_unify_fail is now available as

 configuration option "unify_trace_failure" (global context only).

 * SELECT_GOAL now retains the syntactic context of the overall goal

 state (schematic variables etc.).  Potential INCOMPATIBILITY in rare

 situations.

 *** HOL ***

 * Stronger precedence of syntax for big intersection and union on

 sets, in accordance with corresponding lattice operations.

 INCOMPATIBILITY.

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

 * Nested case expressions are now translated in a separate check phase

 rather than during parsing. The data for case combinators is separated

 from the datatype package. The declaration attribute

 "case_translation" can be used to register new case combinators:

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

 * Code generator:

   - 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' /

     'code_instance'.

   - 'code_identifier' declares name hints for arbitrary identifiers in

     generated code, subsuming 'code_modulename'.

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

 examples.

 * Attibute 'code': 'code' now declares concrete and abstract code

 equations uniformly.  Use explicit 'code equation' and 'code abstract'

 to distinguish both when desired.

 * Discontinued theories Code_Integer and Efficient_Nat by a more

 fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,

 Code_Target_Nat and Code_Target_Numeral.  See the tutorial on code

 generation for details.  INCOMPATIBILITY.

 * Numeric types are mapped by default to target language numerals:

 natural (replaces former code_numeral) and integer (replaces former

 code_int).  Conversions are available as integer_of_natural /

 natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and

 Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in

 ML).  INCOMPATIBILITY.

 * Function package: For mutually recursive functions f and g, separate

 cases rules f.cases and g.cases are generated instead of unusable

 f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,

 in the case that the unusable rule was used nevertheless.

 * Function package: For each function f, new rules f.elims are

 generated, which eliminate equalities of the form "f x = t".

 * New command 'fun_cases' derives ad-hoc elimination rules for

 function equations as simplified instances of f.elims, analogous to

 inductive_cases.  See ~~/src/HOL/ex/Fundefs.thy for some examples.

 * Lifting:

   - parametrized correspondence relations are now supported:

     + parametricity theorems for the raw term can be specified in

       the command lift_definition, which allow us to generate stronger

       transfer rules

     + setup_lifting generates stronger transfer rules if parametric

       correspondence relation can be generated

     + various new properties of the relator must be specified to support

       parametricity

     + parametricity theorem for the Quotient relation can be specified

   - setup_lifting generates domain rules for the Transfer package

   - stronger reflexivity prover of respectfulness theorems for type

     copies

   - ===> and --> are now local. The symbols can be introduced

     by interpreting the locale lifting_syntax (typically in an

     anonymous context)

   - Lifting/Transfer relevant parts of Library/Quotient_* are now in

     Main. Potential INCOMPATIBILITY

   - new commands for restoring and deleting Lifting/Transfer context:

     lifting_forget, lifting_update

   - the command print_quotmaps was renamed to print_quot_maps.

     INCOMPATIBILITY

 * Transfer:

   - better support for domains in Transfer: replace Domainp T

     by the actual invariant in a transferred goal

   - transfer rules can have as assumptions other transfer rules

   - Experimental support for transferring from the raw level to the

     abstract level: Transfer.transferred attribute

   - Attribute version of the transfer method: untransferred attribute

 * Reification and reflection:

   - Reification is now directly available in HOL-Main in structure

     "Reification".

   - Reflection now handles multiple lists with variables also.

   - The whole reflection stack has been decomposed into conversions.

 INCOMPATIBILITY.

 * Revised devices for recursive definitions over finite sets:

   - Only one fundamental fold combinator on finite set remains:

     Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b

     This is now identity on infinite sets.

   - Locales ("mini packages") for fundamental definitions with

     Finite_Set.fold: folding, folding_idem.

   - Locales comm_monoid_set, semilattice_order_set and

     semilattice_neutr_order_set for big operators on sets.

     See theory Big_Operators for canonical examples.

     Note that foundational constants comm_monoid_set.F and

     semilattice_set.F correspond to former combinators fold_image

     and fold1 respectively.  These are now gone.  You may use

     those foundational constants as substitutes, but it is

     preferable to interpret the above locales accordingly.

   - Dropped class ab_semigroup_idem_mult (special case of lattice,

     no longer needed in connection with Finite_Set.fold etc.)

   - Fact renames:

       card.union_inter ~> card_Un_Int [symmetric]

       card.union_disjoint ~> card_Un_disjoint

 INCOMPATIBILITY.

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

 * Complete_Partial_Order.admissible is defined outside the type class

 ccpo, but with mandatory prefix ccpo. Admissibility theorems lose the

 class predicate assumption or sort constraint when possible.

 INCOMPATIBILITY.

 * Introduce type class "conditionally_complete_lattice": Like a

 complete lattice but does not assume the existence of the top and

 bottom elements.  Allows to generalize some lemmas about reals and

 extended reals.  Removed SupInf and replaced it by the instantiation

 of conditionally_complete_lattice for real. Renamed lemmas about

 conditionally-complete lattice from Sup_... to cSup_... and from

 Inf_...  to cInf_... to avoid hidding of similar complete lattice

 lemmas.

 * Introduce type class linear_continuum as combination of

 conditionally-complete lattices and inner dense linorders which have

 more than one element.  INCOMPATIBILITY.

 * Introduced type classes order_top and order_bot. The old classes top

 and bot only contain the syntax without assumptions.  INCOMPATIBILITY:

 Rename bot -> order_bot, top -> order_top

 * Introduce type classes "no_top" and "no_bot" for orderings without

 top and bottom elements.

 * Split dense_linorder into inner_dense_order and no_top, no_bot.

 * Complex_Main: Unify and move various concepts from

 HOL-Multivariate_Analysis to HOL-Complex_Main.

  - Introduce type class (lin)order_topology and

    linear_continuum_topology.  Allows to generalize theorems about

    limits and order.  Instances are reals and extended reals.

  - continuous and continuos_on from Multivariate_Analysis:

    "continuous" is the continuity of a function at a filter.  "isCont"

    is now an abbrevitation: "isCont x f == continuous (at _) f".

    Generalized continuity lemmas from isCont to continuous on an

    arbitrary filter.

  - compact from Multivariate_Analysis. Use Bolzano's lemma to prove

    compactness of closed intervals on reals. Continuous functions

    attain infimum and supremum on compact sets. The inverse of a

    continuous function is continuous, when the function is continuous

    on a compact set.

  - connected from Multivariate_Analysis. Use it to prove the

    intermediate value theorem. Show connectedness of intervals on

    linear_continuum_topology).

  - first_countable_topology from Multivariate_Analysis. Is used to

    show equivalence of properties on the neighbourhood filter of x and

    on all sequences converging to x.

  - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved

    theorems from Library/FDERIV.thy to Deriv.thy and base the

    definition of DERIV on FDERIV. Add variants of DERIV and FDERIV

    which are restricted to sets, i.e. to represent derivatives from

    left or right.

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

      F within X = inf F (principal X)

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

    abbreviation for "at x within UNIV"

  - Introduce named theorem collections tendsto_intros,

    continuous_intros, continuous_on_intros and FDERIV_intros. Theorems

    in tendsto_intros (or FDERIV_intros) are also available as

    tendsto_eq_intros (or FDERIV_eq_intros) where the right-hand side

    is replaced by a congruence rule. This allows to apply them as

    intro rules and then proving equivalence by the simplifier.

  - Restructured theories in HOL-Complex_Main:

    + Moved RealDef and RComplete into Real

    + Introduced Topological_Spaces and moved theorems about

      topological spaces, filters, limits and continuity to it

    + Renamed RealVector to Real_Vector_Spaces

    + Split Lim, SEQ, Series into Topological_Spaces,

      Real_Vector_Spaces, and Limits

    + Moved Ln and Log to Transcendental

    + Moved theorems about continuity from Deriv to Topological_Spaces

  - Remove various auxiliary lemmas.

 INCOMPATIBILITY.

 * Nitpick:

   - Added option "spy".

   - Reduce incidence of "too high arity" errors.

 * Sledgehammer:

   - Renamed option:

       isar_shrink ~> isar_compress

     INCOMPATIBILITY.

   - Added options "isar_try0", "spy".

   - Better support for "isar_proofs".

   - MaSh has been fined-tuned and now runs as a local server.

 * Improved support for ad hoc overloading of constants (see also

 isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).

 * Library/Polynomial.thy:

   - Use lifting for primitive definitions.

   - Explicit conversions from and to lists of coefficients, used for

     generated code.

   - Replaced recursion operator poly_rec by fold_coeffs.

   - Prefer pre-existing gcd operation for gcd.

   - Fact renames:

     poly_eq_iff ~> poly_eq_poly_eq_iff

     poly_ext ~> poly_eqI

     expand_poly_eq ~> poly_eq_iff

 IMCOMPATIBILITY.

 * New Library/Simps_Case_Conv.thy: Provides commands simps_of_case and

 case_of_simps to convert function definitions between a list of

 equations with patterns on the lhs and a single equation with case

 expressions on the rhs. See also Ex/Simps_Case_Conv_Examples.thy.

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

 sets defined by Lifting/Transfer.

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

 * Consolidation of library theories on product orders:

     Product_Lattice ~> Product_Order -- pointwise order on products

     Product_ord ~> Product_Lexorder -- lexicographic order on products

 INCOMPATIBILITY.

 * Imperative-HOL: The MREC combinator is considered legacy and no

 longer included by default. INCOMPATIBILITY, use partial_function

 instead, or import theory Legacy_Mrec as a fallback.

 * HOL-Algebra: Discontinued theories ~~/src/HOL/Algebra/abstract and

 ~~/src/HOL/Algebra/poly.  Existing theories should be based on

 ~~/src/HOL/Library/Polynomial instead.  The latter provides

 integration with HOL's type classes for rings.  INCOMPATIBILITY.

 * HOL-BNF:

   - Various improvements to BNF-based (co)datatype package, including

     new commands "primrec_new", "primcorec", and

     "datatype_new_compat", as well as documentation. See

     "datatypes.pdf" for details.

   - New "coinduction" method to avoid some boilerplate (compared to

     coinduct).

   - Renamed keywords:

     data ~> datatype_new

     codata ~> codatatype

     bnf_def ~> bnf

   - Renamed many generated theorems, including

     discs ~> disc

     map_comp' ~> map_comp

     map_id' ~> map_id

     sels ~> sel

     set_map' ~> set_map

     sets ~> set

 IMCOMPATIBILITY.

 *** ML ***

 * Spec_Check is a Quickcheck tool for Isabelle/ML.  The ML function

 "check_property" allows to check specifications of the form "ALL x y

 z. prop x y z".  See also ~~/src/Tools/Spec_Check/ with its

 Examples.thy in particular.

 * Improved printing of exception trace in Poly/ML 5.5.1, with regular

 tracing output in the command transaction context instead of physical

 stdout.  See also Toplevel.debug, Toplevel.debugging and

 ML_Compiler.exn_trace.

 * 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