diff r 740c70a21523 r 038ee85c95e4 NEWS
 a/NEWS Thu Dec 31 21:06:09 2015 +0100
+++ b/NEWS Thu Dec 31 21:24:58 2015 +0100
@@ 9,6 +9,18 @@
*** General ***
+* Former "xsymbols" syntax with Isabelle symbols is used by default,
+without any special print mode. Important ASCII replacement syntax
+remains available under print mode "ASCII", but less important syntax
+has been removed (see below).
+
+* Support for more arrow symbols, with rendering in LaTeX and
+Isabelle fonts: \ \ \ \ \ \
+
+* Syntax for formal comments " text" now also supports the symbolic
+form "\ text". Commandline tool "isabelle update_cartouches c" helps
+to update old sources.
+
* Toplevel theorem statements have been simplified as follows:
theorems ~> lemmas
@@ 22,31 +34,9 @@
* Toplevel theorem statement 'proposition' is another alias for
'theorem'.
* Syntax for formal comments " text" now also supports the symbolic
form "\ text". Commandline tool "isabelle update_cartouches c" helps
to update old sources.

* Former "xsymbols" syntax with Isabelle symbols is used by default,
without any special print mode. Important ASCII replacement syntax
remains available under print mode "ASCII", but less important syntax
has been removed (see below).

* Support for more arrow symbols, with rendering in LaTeX and
Isabelle fonts: \ \ \ \ \ \

*** Prover IDE  Isabelle/Scala/jEdit ***
* Completion of symbols via prefix of \ or \<^name> or \name is
always possible, independently of the language context. It is never
implicit: a popup will show up unconditionally.

* Additional abbreviations for syntactic completion may be specified in
$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs.

* Improved scheduling for urgent print tasks (e.g. command state output,
interactive queries) wrt. longrunning background tasks.

* IDE support for the sourcelevel 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',
@@ 56,9 +46,6 @@
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 singleinstance Desktop
application uniformly on all platforms: Linux, Windows, Mac OS X.

* The State panel manages explicit proof state output, with dynamic
autoupdate according to cursor movement. Alternatively, the jEdit
action "isabelle.updatestate" (shortcut S+ENTER) triggers manual
@@ 80,6 +67,17 @@
due to adhoc updates by auxiliary GUI components, such as the State
panel.
+* Improved scheduling for urgent print tasks (e.g. command state output,
+interactive queries) wrt. longrunning background tasks.
+
+* Completion of symbols via prefix of \ or \<^name> or \name is
+always possible, independently of the language context. It is never
+implicit: a popup will show up unconditionally.
+
+* Additional abbreviations for syntactic completion may be specified in
+$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with
+support for simple templates using ASCII 007 (bell) as placeholder.
+
* Action "isabelleemph" (with keyboard shortcut C+e LEFT) controls
emphasized text style; the effect is visible in document output, not in
the editor.
@@ 87,15 +85,18 @@
* Action "isabellereset" now uses keyboard shortcut C+e BACK_SPACE,
instead of former C+e LEFT.
* New commandline tool "isabelle jedit_client" allows to connect to an
already running Isabelle/jEdit process. This achieves the effect of
singleinstance applications seen on common GUI desktops.

* The commandline tool "isabelle jedit" and the isabelle.Main
application wrapper threat the default $USER_HOME/Scratch.thy more
uniformly, and allow the dummy file argument ":" to open an empty buffer
instead.
+* New commandline tool "isabelle jedit_client" allows to connect to an
+already running Isabelle/jEdit process. This achieves the effect of
+singleinstance applications seen on common GUI desktops.
+
+* The main Isabelle executable is managed as singleinstance Desktop
+application uniformly on all platforms: Linux, Windows, Mac OS X.
+
* The default lookandfeel for Linux is the traditional "Metal", which
works better with GUI scaling for very highresolution displays (e.g.
4K). Moreover, it is generally more robust than "Nimbus".
@@ 103,6 +104,21 @@
*** Document preparation ***
+* Commands 'paragraph' and 'subparagraph' provide additional section
+headings. Thus there are 6 levels of standard headings, as in HTML.
+
+* Command 'text_raw' has been clarified: input text is processed as in
+'text' (with antiquotations and control symbols). The key difference is
+the lack of the surrounding isabelle markup environment in output.
+
+* Text is structured in paragraphs and nested lists, using notation that
+is similar to Markdown. The control symbols for list items are as
+follows:
+
+ \<^item> itemize
+ \<^enum> enumerate
+ \<^descr> description
+
* There is a new short form for antiquotations with a single argument
that is a cartouche: \<^name>\...\ is equivalent to @{name \...\} and
\...\ without control symbol is equivalent to @{cartouche \...\}.
@@ 110,18 +126,6 @@
standard Isabelle fonts provide glyphs to render important control
symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
* Antiquotation @{theory_text} prints uninterpreted theory source text
(outer syntax with command keywords etc.). This may be used in the short
form \<^theory_text>\...\. @{theory_text [display]} supports option "indent".

* @{verbatim [display]} supports option "indent".

* Antiquotation @{doc ENTRY} provides a reference to the given
documentation, with a hyperlink in the Prover IDE.

* Antiquotations @{command}, @{method}, @{attribute} print checked
entities of the Isar language.

* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with
corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using
standard LaTeX macros of the same names.
@@ 138,44 +142,32 @@
argument where they are really intended, e.g. @{text \"foo"\}. Initial
or terminal spaces are ignored.
+* Antiquotations @{emph} and @{bold} output LaTeX source recursively,
+adding appropriate text style markup. These may be used in the short
+form \<^emph>\...\ and \<^bold>\...\.
+
+* Document antiquotation @{footnote} outputs LaTeX source recursively,
+marked as \footnote{}. This may be used in the short form \<^footnote>\...\.
+
+* Antiquotation @{verbatim [display]} supports option "indent".
+
+* Antiquotation @{theory_text} prints uninterpreted theory source text
+(outer syntax with command keywords etc.). This may be used in the short
+form \<^theory_text>\...\. @{theory_text [display]} supports option "indent".
+
+* Antiquotation @{doc ENTRY} provides a reference to the given
+documentation, with a hyperlink in the Prover IDE.
+
+* Antiquotations @{command}, @{method}, @{attribute} print checked
+entities of the Isar language.
+
* HTML presentation uses the standard IsabelleText font and Unicode
rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former
print mode "HTML" loses its special meaning.
* Commands 'paragraph' and 'subparagraph' provide additional section
headings. Thus there are 6 levels of standard headings, as in HTML.

* Text is structured in paragraphs and nested lists, using notation that
is similar to Markdown. The control symbols for list items are as
follows:

 \<^item> itemize
 \<^enum> enumerate
 \<^descr> description

* Command 'text_raw' has been clarified: input text is processed as in
'text' (with antiquotations and control symbols). The key difference is
the lack of the surrounding isabelle markup environment in output.

* Document antiquotations @{emph} and @{bold} output LaTeX source
recursively, adding appropriate text style markup. These may be used in
the short form \<^emph>\...\ and \<^bold>\...\.

* Document antiquotation @{footnote} outputs LaTeX source recursively,
marked as \footnote{}. This may be used in the short form \<^footnote>\...\.

*** Isar ***
* Command 'obtain' binds term abbreviations (via 'is' patterns) in the
proof body as well, abstracted over relevant parameters.

* Improved typeinference 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
rule statements like fixes/assumes/shows in theorem specifications, but
the notation is postfix with keywords 'if' (or 'when') and 'for'. For
@@ 234,9 +226,6 @@
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 multibranch 'obtain' without activation
@@ 274,11 +263,36 @@
is still available as legacy for some time. Documentation now explains
'..' more accurately as "by standard" instead of "by rule".
+* 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 \ A" if a: A for A
+ supply [simp] = a
+ proof
+ show A by simp
+ next
+ show A by simp
+ qed
+
+* Command 'obtain' binds term abbreviations (via 'is' patterns) in the
+proof body as well, abstracted over relevant parameters.
+
+* Improved typeinference 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.
+
* 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 isarref
manual.
+* Command 'supply' supports fact definitions during goal refinement
+('apply' scripts).
+
* 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:
@@ 308,18 +322,8 @@
"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 \ A" if a: A for A
 supply [simp] = a
 proof
 show A by simp
 next
 show A by simp
 qed
+* The vacuous fact "TERM x" may be established "by fact" or as `TERM x`
+as well, not just "by this" or "." as before.
* Method "sleep" succeeds after a realtime delay (in seconds). This is
occasionally useful for demonstration and testing purposes.
@@ 333,17 +337,16 @@
INCOMPATIBILITY, remove '!' and add '?' as required.
* Keyword 'rewrites' identifies rewrite morphisms in interpretation
commands. Previously, the keyword was 'where'. INCOMPATIBILITY.
+commands. Previously, the keyword was 'where'. INCOMPATIBILITY.
* More gentle suppression of syntax along locale morphisms while
printing terms. Previously 'abbreviation' and 'notation' declarations
would be suppressed for morphisms except term identity. Now
+printing terms. Previously 'abbreviation' and 'notation' declarations
+would be suppressed for morphisms except term identity. Now
'abbreviation' is also kept for morphims that only change the involved
parameters, and only 'notation' is suppressed. This can be of great
help when working with complex locale hierarchies, because proof
states are displayed much more succinctly. It also means that only
notation needs to be redeclared if desired, as illustrated by this
example:
+parameters, and only 'notation' is suppressed. This can be of great help
+when working with complex locale hierarchies, because proof states are
+displayed much more succinctly. It also means that only notation needs
+to be redeclared if desired, as illustrated by this example:
locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\" 65)
begin
@@ 369,11 +372,8 @@
* 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.
+(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY.
* Abbreviations in type classes now carry proper sort constraint.
Rare INCOMPATIBILITY in situations where the previous misbehaviour
@@ 386,9 +386,71 @@
*** HOL ***
* Combinator to represent case distinction on products is named "case_prod",
uniformly, discontinuing any input aliasses. Very popular theorem aliasses
have been retained.
+* 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
+oldstyle "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:
+
+ notation iff (infixr "<>" 25)
+
+ notation Times (infixr "<*>" 80)
+
+ 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)
+
+ notation (in topological_space) tendsto (infixr ">" 55)
+ notation (in topological_space) LIMSEQ ("((_)/ > (_))" [60, 60] 60)
+ notation LIM ("((_)/  (_)/ > (_))" [60, 0, 60] 60)
+
+ notation NSA.approx (infixl "@=" 50)
+ notation NSLIMSEQ ("((_)/ NS> (_))" [60, 60] 60)
+ notation NSLIM ("((_)/  (_)/ NS> (_))" [60, 0, 60] 60)
+
+* The alternative notation "\" for type and sort constraints has been
+removed: in LaTeX document output it looks the same as "::".
+INCOMPATIBILITY, use plain "::" instead.
+
+* 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".
+
+* Inductive definitions ('inductive', 'coinductive', etc.) expose
+lowlevel facts of the internal construction only if the option
+"inductive_defs" is enabled. This refers to the internal predicate
+definition and its monotonicity result. Rare INCOMPATIBILITY.
+
+* Recursive function definitions ('fun', 'function', 'partial_function')
+expose lowlevel facts of the internal construction only if the option
+"function_defs" is enabled. Rare INCOMPATIBILITY.
+
+* 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
@@ 425,36 +487,21 @@
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
oldstyle "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.

* The coercions to type 'real' have been reorganised. The function 'real'
is no longer overloaded, but has type 'nat => real' and abbreviates
of_nat for that type. Also 'real_of_int :: int => real' abbreviates
of_int for that type. Other overloaded instances of 'real' have been
replaced by 'real_of_ereal' and 'real_of_float'.
+
+INCOMPATIBILITY.
+
+* The coercions to type 'real' have been reorganised. The function
+'real' is no longer overloaded, but has type 'nat => real' and
+abbreviates of_nat for that type. Also 'real_of_int :: int => real'
+abbreviates of_int for that type. Other overloaded instances of 'real'
+have been replaced by 'real_of_ereal' and 'real_of_float'.
+
Consolidated facts (among others):
real_of_nat_le_iff > of_nat_le_iff
real_of_nat_numeral of_nat_numeral
@@ 478,41 +525,8 @@
floor_divide_eq_div floor_divide_of_int_eq
real_of_int_zero_cancel of_nat_eq_0_iff
ceiling_real_of_int ceiling_of_int
INCOMPATIBILITY.

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

 notation iff (infixr "<>" 25)

 notation Times (infixr "<*>" 80)

 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)

 notation (in topological_space) tendsto (infixr ">" 55)
 notation (in topological_space) LIMSEQ ("((_)/ > (_))" [60, 60] 60)
 notation LIM ("((_)/  (_)/ > (_))" [60, 0, 60] 60)

 notation NSA.approx (infixl "@=" 50)
 notation NSLIMSEQ ("((_)/ NS> (_))" [60, 60] 60)
 notation NSLIM ("((_)/  (_)/ NS> (_))" [60, 0, 60] 60)

* The alternative notation "\" for type and sort constraints has been
removed: in LaTeX document output it looks the same as "::".
INCOMPATIBILITY, use plain "::" instead.
+
+INCOMPATIBILITY.
* Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has
been removed. INCOMPATIBILITY.
@@ 551,38 +565,38 @@
'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
+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. Minor
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.
+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.

* New cancellation simprocs for boolean algebras to cancel
complementary terms for sup and inf. For example, "sup x (sup y ( x))"
simplifies to "top". INCOMPATIBILITY.
+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.
+
+* New cancellation simprocs for boolean algebras to cancel complementary
+terms for sup and inf. For example, "sup x (sup y ( x))" simplifies to
+"top". INCOMPATIBILITY.
* Library/Multiset:
 Renamed multiset inclusion operators:
@@ 614,36 +628,27 @@
less_eq_multiset_def
INCOMPATIBILITY
* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the BourbakiWitt
fixpoint theorem for increasing functions in chaincomplete partial
orders.

* Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= complex path integrals),
Cauchy's integral theorem, winding numbers and Cauchy's integral formula, Liouville theorem,
Fundamental Theorem of Algebra. Ported from HOL Light

* Multivariate_Analysis: Added topological concepts such as connected components,
homotopic paths and the inside or outside of a set.

* Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
command. Minor INCOMPATIBILITY, use 'function' instead.

* Inductive definitions ('inductive', 'coinductive', etc.) expose
lowlevel facts of the internal construction only if the option
"inductive_defs" is enabled. This refers to the internal predicate
definition and its monotonicity result. Rare INCOMPATIBILITY.

* Recursive function definitions ('fun', 'function', 'partial_function')
expose lowlevel facts of the internal construction only if the option
"function_defs" is enabled. Rare INCOMPATIBILITY.
+* Library/Omega_Words_Fun: Infinite words modeled as functions nat \ 'a.
+
+* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the
+BourbakiWitt fixpoint theorem for increasing functions in
+chaincomplete partial orders.
+
+* Library/Old_Recdef: discontinued obsolete 'defer_recdef' command.
+Minor INCOMPATIBILITY, use 'function' instead.
+
+* Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (=
+complex path integrals), Cauchy's integral theorem, winding numbers and
+Cauchy's integral formula, Liouville theorem, Fundamental Theorem of
+Algebra. Ported from HOL Light
+
+* Multivariate_Analysis: Added topological concepts such as connected
+components, homotopic paths and the inside or outside of a set.
* Data_Structures: new and growing session of standard data structures.
* Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
* Library/Omega_Words_Fun: Infinite words modeled as functions nat =>
'a.

* HOLStatespace: command 'statespace' uses mandatory qualifier for
import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
remove '!' and add '?' as required.
@@ 651,18 +656,19 @@
*** ML ***
+* The following combinators for lowlevel profiling of the ML runtime
+system are available:
+
+ profile_time (*CPU time*)
+ profile_time_thread (*CPU time on this thread*)
+ profile_allocations (*overall heap allocations*)
+
+* Antiquotation @{undefined} or \<^undefined> inlines (raise Match).
+
* Pretty printing of Poly/ML compiler output in Isabelle has been
improved: proper treatment of break offsets and blocks with consistent
breaks.
* Isar proof methods are based on a slightly more general type
context_tactic, which allows to change the proof context dynamically
(e.g. to update cases) and indicate explicit Seq.Error results. Former
METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are
provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY.

* Antiquotation @{undefined} or \<^undefined> inlines (raise Match).

* 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.
@@ 698,18 +704,26 @@
tools, but can also cause INCOMPATIBILITY for tools that don't observe
the proof context discipline.
* The following combinators for lowlevel profiling of the ML runtime
system are available:

 profile_time (*CPU time*)
 profile_time_thread (*CPU time on this thread*)
 profile_allocations (*overall heap allocations*)
+* Isar proof methods are based on a slightly more general type
+context_tactic, which allows to change the proof context dynamically
+(e.g. to update cases) and indicate explicit Seq.Error results. Former
+METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are
+provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY.
*** System ***
* Commandline tool "isabelle console" enables print mode "ASCII".
+* Commandline 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.
+
* Global session timeout is multiplied by timeout_scale factor. This
allows to adjust largescale tests (e.g. AFP) to overall hardware
performance.
@@ 719,22 +733,6 @@
\ code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono
* Commandline 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.6 runs natively on x86windows and x86_64windows, which
both allow larger heap space than former x86cygwin.

* Java runtime environment for x86_64windows allows to use larger heap
space.
@@ 757,6 +755,13 @@
* Heap images are 1015% smaller due to less wasteful persistent theory
content (using ML type theory_id instead of theory);
+* 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.6 runs natively on x86windows and x86_64windows, which
+both allow larger heap space than former x86cygwin.
+
New in Isabelle2015 (May 2015)