merged
authorwenzelm
Thu Apr 02 13:41:31 2009 +0200 (2009-04-02)
changeset 30846fd8ed5a39a8e
parent 30844 7d0e10a961a6
parent 30845 9a887484de53
child 30847 dd9a1662413b
merged
     1.1 --- a/NEWS	Wed Apr 01 22:29:27 2009 +0200
     1.2 +++ b/NEWS	Thu Apr 02 13:41:31 2009 +0200
     1.3 @@ -1,15 +1,11 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 -New in this Isabelle version
     1.8 -----------------------------
     1.9 +New in Isabelle2009 (April 2009)
    1.10 +--------------------------------
    1.11  
    1.12  *** General ***
    1.13  
    1.14 -* The main reference manuals (isar-ref, implementation, system) have
    1.15 -been updated and extended.  Formally checked references as hyperlinks
    1.16 -are now available in uniform manner.
    1.17 -
    1.18  * Simplified main Isabelle executables, with less surprises on
    1.19  case-insensitive file-systems (such as Mac OS).
    1.20  
    1.21 @@ -37,110 +33,31 @@
    1.22  install -p ...", or use symlinks.
    1.23  
    1.24  * The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
    1.25 -old ~/isabelle, which was slightly non-standard and apt cause
    1.26 -surprises on case-insensitive file-systems.
    1.27 +old ~/isabelle, which was slightly non-standard and apt to cause
    1.28 +surprises on case-insensitive file-systems (such as Mac OS).
    1.29  
    1.30  INCOMPATIBILITY, need to move existing ~/isabelle/etc,
    1.31  ~/isabelle/heaps, ~/isabelle/browser_info to the new place.  Special
    1.32  care is required when using older releases of Isabelle.  Note that
    1.33  ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any
    1.34 -Isabelle distribution.
    1.35 +Isabelle distribution, in order to use the new ~/.isabelle uniformly.
    1.36  
    1.37  * Proofs of fully specified statements are run in parallel on
    1.38 -multi-core systems.  A speedup factor of 2-3 can be expected on a
    1.39 -regular 4-core machine, if the initial heap space is made reasonably
    1.40 -large (cf. Poly/ML option -H).  [Poly/ML 5.2.1 or later]
    1.41 -
    1.42 -* Generalized Isar history, with support for linear undo, direct state
    1.43 -addressing etc.
    1.44 -
    1.45 -* Recovered hiding of consts, which was accidentally broken in
    1.46 -Isabelle2007.  Potential INCOMPATIBILITY, ``hide const c'' really
    1.47 -makes c inaccessible; consider using ``hide (open) const c'' instead.
    1.48 -
    1.49 -* Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
    1.50 -interface instead.
    1.51 -
    1.52 -* There is a new syntactic category "float_const" for signed decimal
    1.53 -fractions (e.g. 123.45 or -123.45).
    1.54 -
    1.55 -* New prover for coherent logic (see src/Tools/coherent.ML).
    1.56 +multi-core systems.  A speedup factor of 2.5 to 3.2 can be expected on
    1.57 +a regular 4-core machine, if the initial heap space is made reasonably
    1.58 +large (cf. Poly/ML option -H).  (Requires Poly/ML 5.2.1 or later.)
    1.59 +
    1.60 +* The main reference manuals ("isar-ref", "implementation", and
    1.61 +"system") have been updated and extended.  Formally checked references
    1.62 +as hyperlinks are now available uniformly.
    1.63 +
    1.64  
    1.65  
    1.66  *** Pure ***
    1.67  
    1.68 -* Class declaration: sc. "base sort" must not be given in import list
    1.69 -any longer but is inferred from the specification.  Particularly in HOL,
    1.70 -write
    1.71 -
    1.72 -    class foo = ...     instead of      class foo = type + ...
    1.73 -
    1.74 -* Module moves in repository:
    1.75 -    src/Pure/Tools/value.ML ~> src/Tools/
    1.76 -    src/Pure/Tools/quickcheck.ML ~> src/Tools/
    1.77 -
    1.78 -* Slightly more coherent Pure syntax, with updated documentation in
    1.79 -isar-ref manual.  Removed locales meta_term_syntax and
    1.80 -meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,
    1.81 -INCOMPATIBILITY in rare situations.
    1.82 -
    1.83 -* Goal-directed proof now enforces strict proof irrelevance wrt. sort
    1.84 -hypotheses.  Sorts required in the course of reasoning need to be
    1.85 -covered by the constraints in the initial statement, completed by the
    1.86 -type instance information of the background theory.  Non-trivial sort
    1.87 -hypotheses, which rarely occur in practice, may be specified via
    1.88 -vacuous propositions of the form SORT_CONSTRAINT('a::c).  For example:
    1.89 -
    1.90 -  lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ...
    1.91 -
    1.92 -The result contains an implicit sort hypotheses as before --
    1.93 -SORT_CONSTRAINT premises are eliminated as part of the canonical rule
    1.94 -normalization.
    1.95 -
    1.96 -* Changed defaults for unify configuration options:
    1.97 -
    1.98 -  unify_trace_bound = 50 (formerly 25)
    1.99 -  unify_search_bound = 60 (formerly 30)
   1.100 -
   1.101 -* Different bookkeeping for code equations (INCOMPATIBILITY):
   1.102 -
   1.103 -  a) On theory merge, the last set of code equations for a particular
   1.104 -     constant is taken (in accordance with the policy applied by other
   1.105 -     parts of the code generator framework).
   1.106 -
   1.107 -  b) Code equations stemming from explicit declarations (e.g. code
   1.108 -     attribute) gain priority over default code equations stemming
   1.109 -     from definition, primrec, fun etc.
   1.110 -
   1.111 -* Global versions of theorems stemming from classes do not carry a
   1.112 -parameter prefix any longer.  INCOMPATIBILITY.
   1.113 -
   1.114 -* Dropped locale element "includes".  This is a major INCOMPATIBILITY.
   1.115 -In existing theorem specifications replace the includes element by the
   1.116 -respective context elements of the included locale, omitting those
   1.117 -that are already present in the theorem specification.  Multiple
   1.118 -assume elements of a locale should be replaced by a single one
   1.119 -involving the locale predicate.  In the proof body, declarations (most
   1.120 -notably theorems) may be regained by interpreting the respective
   1.121 -locales in the proof context as required (command "interpret").
   1.122 -
   1.123 -If using "includes" in replacement of a target solely because the
   1.124 -parameter types in the theorem are not as general as in the target,
   1.125 -consider declaring a new locale with additional type constraints on
   1.126 -the parameters (context element "constrains").
   1.127 -
   1.128 -* Dropped "locale (open)".  INCOMPATIBILITY.
   1.129 -
   1.130 -* Interpretation commands no longer attempt to simplify goal.
   1.131 -INCOMPATIBILITY: in rare situations the generated goal differs.  Use
   1.132 -methods intro_locales and unfold_locales to clarify.
   1.133 -
   1.134 -* Interpretation commands no longer accept interpretation attributes.
   1.135 -INCOMPATBILITY.
   1.136 -
   1.137 -* Complete re-implementation of locales.  INCOMPATIBILITY.  The most
   1.138 -important changes are listed below.  See the Tutorial on Locales for
   1.139 -details.
   1.140 +* Complete re-implementation of locales.  INCOMPATIBILITY in several
   1.141 +respects.  The most important changes are listed below.  See the
   1.142 +Tutorial on Locales ("locales" manual) for details.
   1.143  
   1.144  - In locale expressions, instantiation replaces renaming.  Parameters
   1.145  must be declared in a for clause.  To aid compatibility with previous
   1.146 @@ -158,35 +75,116 @@
   1.147  optional (syntax "name?:").  The default depends for plain "name:"
   1.148  depends on the situation where a locale expression is used: in
   1.149  commands 'locale' and 'sublocale' prefixes are optional, in
   1.150 -'interpretation' and 'interpret' prefixes are mandatory.  Old-style
   1.151 +'interpretation' and 'interpret' prefixes are mandatory.  The old
   1.152  implicit qualifiers derived from the parameter names of a locale are
   1.153  no longer generated.
   1.154  
   1.155 -- "sublocale l < e" replaces "interpretation l < e".  The
   1.156 +- Command "sublocale l < e" replaces "interpretation l < e".  The
   1.157  instantiation clause in "interpretation" and "interpret" (square
   1.158  brackets) is no longer available.  Use locale expressions.
   1.159  
   1.160 -- When converting proof scripts, be sure to mandatory qualifiers in
   1.161 +- When converting proof scripts, mandatory qualifiers in
   1.162  'interpretation' and 'interpret' should be retained by default, even
   1.163 -if this is an INCOMPATIBILITY compared to former behaviour.
   1.164 -Qualifiers in locale expressions range over a single locale instance
   1.165 -only.
   1.166 -
   1.167 -* Command 'instance': attached definitions no longer accepted.
   1.168 -INCOMPATIBILITY, use proper 'instantiation' target.
   1.169 -
   1.170 -* Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
   1.171 +if this is an INCOMPATIBILITY compared to former behavior.  In the
   1.172 +worst case, use the "name?:" form for non-mandatory ones.  Qualifiers
   1.173 +in locale expressions range over a single locale instance only.
   1.174 +
   1.175 +- Dropped locale element "includes".  This is a major INCOMPATIBILITY.
   1.176 +In existing theorem specifications replace the includes element by the
   1.177 +respective context elements of the included locale, omitting those
   1.178 +that are already present in the theorem specification.  Multiple
   1.179 +assume elements of a locale should be replaced by a single one
   1.180 +involving the locale predicate.  In the proof body, declarations (most
   1.181 +notably theorems) may be regained by interpreting the respective
   1.182 +locales in the proof context as required (command "interpret").
   1.183 +
   1.184 +If using "includes" in replacement of a target solely because the
   1.185 +parameter types in the theorem are not as general as in the target,
   1.186 +consider declaring a new locale with additional type constraints on
   1.187 +the parameters (context element "constrains").
   1.188 +
   1.189 +- Discontinued "locale (open)".  INCOMPATIBILITY.
   1.190 +
   1.191 +- Locale interpretation commands no longer attempt to simplify goal.
   1.192 +INCOMPATIBILITY: in rare situations the generated goal differs.  Use
   1.193 +methods intro_locales and unfold_locales to clarify.
   1.194 +
   1.195 +- Locale interpretation commands no longer accept interpretation
   1.196 +attributes.  INCOMPATIBILITY.
   1.197 +
   1.198 +* Class declaration: so-called "base sort" must not be given in import
   1.199 +list any longer, but is inferred from the specification.  Particularly
   1.200 +in HOL, write
   1.201 +
   1.202 +    class foo = ...
   1.203 +
   1.204 +instead of
   1.205 +
   1.206 +    class foo = type + ...
   1.207 +
   1.208 +* Class target: global versions of theorems stemming do not carry a
   1.209 +parameter prefix any longer.  INCOMPATIBILITY.
   1.210 +
   1.211 +* Class 'instance' command no longer accepts attached definitions.
   1.212 +INCOMPATIBILITY, use proper 'instantiation' target instead.
   1.213 +
   1.214 +* Recovered hiding of consts, which was accidentally broken in
   1.215 +Isabelle2007.  Potential INCOMPATIBILITY, ``hide const c'' really
   1.216 +makes c inaccessible; consider using ``hide (open) const c'' instead.
   1.217 +
   1.218 +* Slightly more coherent Pure syntax, with updated documentation in
   1.219 +isar-ref manual.  Removed locales meta_term_syntax and
   1.220 +meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,
   1.221 +INCOMPATIBILITY in rare situations.  Note that &&& should not be used
   1.222 +directly in regular applications.
   1.223 +
   1.224 +* There is a new syntactic category "float_const" for signed decimal
   1.225 +fractions (e.g. 123.45 or -123.45).
   1.226 +
   1.227 +* Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
   1.228 +interface with 'setup' command instead.
   1.229 +
   1.230 +* Command 'local_setup' is similar to 'setup', but operates on a local
   1.231 +theory context.
   1.232  
   1.233  * The 'axiomatization' command now only works within a global theory
   1.234  context.  INCOMPATIBILITY.
   1.235  
   1.236 -* New 'find_theorems' criterion "solves" matching theorems that
   1.237 -directly solve the current goal.
   1.238 -
   1.239 -* Auto solve feature for main theorem statements (cf. option in Proof
   1.240 -General Isabelle settings menu, disabled by default).  Whenever a new
   1.241 -goal is stated, "find_theorems solves" is called; any theorems that
   1.242 -could solve the lemma directly are listed as part of the goal state.
   1.243 +* Goal-directed proof now enforces strict proof irrelevance wrt. sort
   1.244 +hypotheses.  Sorts required in the course of reasoning need to be
   1.245 +covered by the constraints in the initial statement, completed by the
   1.246 +type instance information of the background theory.  Non-trivial sort
   1.247 +hypotheses, which rarely occur in practice, may be specified via
   1.248 +vacuous propositions of the form SORT_CONSTRAINT('a::c).  For example:
   1.249 +
   1.250 +  lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ...
   1.251 +
   1.252 +The result contains an implicit sort hypotheses as before --
   1.253 +SORT_CONSTRAINT premises are eliminated as part of the canonical rule
   1.254 +normalization.
   1.255 +
   1.256 +* Generalized Isar history, with support for linear undo, direct state
   1.257 +addressing etc.
   1.258 +
   1.259 +* Changed defaults for unify configuration options:
   1.260 +
   1.261 +  unify_trace_bound = 50 (formerly 25)
   1.262 +  unify_search_bound = 60 (formerly 30)
   1.263 +
   1.264 +* Different bookkeeping for code equations (INCOMPATIBILITY):
   1.265 +
   1.266 +  a) On theory merge, the last set of code equations for a particular
   1.267 +     constant is taken (in accordance with the policy applied by other
   1.268 +     parts of the code generator framework).
   1.269 +
   1.270 +  b) Code equations stemming from explicit declarations (e.g. code
   1.271 +     attribute) gain priority over default code equations stemming
   1.272 +     from definition, primrec, fun etc.
   1.273 +
   1.274 +* Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
   1.275 +
   1.276 +* Unified theorem tables for both code code generators.  Thus [code
   1.277 +func] has disappeared and only [code] remains.  INCOMPATIBILITY.
   1.278  
   1.279  * Command 'find_consts' searches for constants based on type and name
   1.280  patterns, e.g.
   1.281 @@ -200,8 +198,15 @@
   1.282  
   1.283      find_consts strict: "_ => bool" name: "Int" -"int => int"
   1.284  
   1.285 -* Command 'local_setup' is similar to 'setup', but operates on a local
   1.286 -theory context.
   1.287 +* New 'find_theorems' criterion "solves" matches theorems that
   1.288 +directly solve the current goal (modulo higher-order unification).
   1.289 +
   1.290 +* Auto solve feature for main theorem statements: whenever a new goal
   1.291 +is stated, "find_theorems solves" is called; any theorems that could
   1.292 +solve the lemma directly are listed as part of the goal state.
   1.293 +Cf. associated options in Proof General Isabelle settings menu,
   1.294 +enabled by default, with reasonable timeout for pathological cases of
   1.295 +higher-order unification.
   1.296  
   1.297  
   1.298  *** Document preparation ***
   1.299 @@ -213,34 +218,84 @@
   1.300  
   1.301  *** HOL ***
   1.302  
   1.303 -* Theory Library/Polynomial.thy defines an abstract type 'a poly of
   1.304 -univariate polynomials with coefficients of type 'a.  In addition to
   1.305 -the standard ring operations, it also supports div and mod.  Code
   1.306 -generation is also supported, using list-style constructors.
   1.307 -
   1.308 -* Theory Library/Inner_Product.thy defines a class of real_inner for
   1.309 -real inner product spaces, with an overloaded operation inner :: 'a =>
   1.310 -'a => real.  Class real_inner is a subclass of real_normed_vector from
   1.311 -RealVector.thy.
   1.312 -
   1.313 -* Theory Library/Product_Vector.thy provides instances for the product
   1.314 -type 'a * 'b of several classes from RealVector.thy and
   1.315 -Inner_Product.thy.  Definitions of addition, subtraction, scalar
   1.316 -multiplication, norms, and inner products are included.
   1.317 -
   1.318 -* Theory Library/Bit.thy defines the field "bit" of integers modulo 2.
   1.319 -In addition to the field operations, numerals and case syntax are also
   1.320 -supported.
   1.321 -
   1.322 -* Theory Library/Diagonalize.thy provides constructive version of
   1.323 -Cantor's first diagonalization argument.
   1.324 -
   1.325 -* New predicate "strict_mono" classifies strict functions on partial orders.
   1.326 -With strict functions on linear orders, reasoning about (in)equalities is
   1.327 -facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less".
   1.328 -
   1.329 -* Some set operations are now proper qualified constants with authentic syntax.
   1.330 -INCOMPATIBILITY:
   1.331 +* Integrated main parts of former image HOL-Complex with HOL.  Entry
   1.332 +points Main and Complex_Main remain as before.
   1.333 +
   1.334 +* Logic image HOL-Plain provides a minimal HOL with the most important
   1.335 +tools available (inductive, datatype, primrec, ...).  This facilitates
   1.336 +experimentation and tool development.  Note that user applications
   1.337 +(and library theories) should never refer to anything below theory
   1.338 +Main, as before.
   1.339 +
   1.340 +* Logic image HOL-Main stops at theory Main, and thus facilitates
   1.341 +experimentation due to shorter build times.
   1.342 +
   1.343 +* Logic image HOL-NSA contains theories of nonstandard analysis which
   1.344 +were previously part of former HOL-Complex.  Entry point Hyperreal
   1.345 +remains valid, but theories formerly using Complex_Main should now use
   1.346 +new entry point Hypercomplex.
   1.347 +
   1.348 +* Generic ATP manager for Sledgehammer, based on ML threads instead of
   1.349 +Posix processes.  Avoids potentially expensive forking of the ML
   1.350 +process.  New thread-based implementation also works on non-Unix
   1.351 +platforms (Cygwin).  Provers are no longer hardwired, but defined
   1.352 +within the theory via plain ML wrapper functions.  Basic Sledgehammer
   1.353 +commands are covered in the isar-ref manual.
   1.354 +
   1.355 +* Wrapper scripts for remote SystemOnTPTP service allows to use
   1.356 +sledgehammer without local ATP installation (Vampire etc.). Other
   1.357 +provers may be included via suitable ML wrappers, see also
   1.358 +src/HOL/ATP_Linkup.thy.
   1.359 +
   1.360 +* ATP selection (E/Vampire/Spass) is now via Proof General's settings
   1.361 +menu.
   1.362 +
   1.363 +* The metis method no longer fails because the theorem is too trivial
   1.364 +(contains the empty clause).
   1.365 +
   1.366 +* The metis method now fails in the usual manner, rather than raising
   1.367 +an exception, if it determines that it cannot prove the theorem.
   1.368 +
   1.369 +* Method "coherent" implements a prover for coherent logic (see also
   1.370 +src/Tools/coherent.ML).
   1.371 +
   1.372 +* Constants "undefined" and "default" replace "arbitrary".  Usually
   1.373 +"undefined" is the right choice to replace "arbitrary", though
   1.374 +logically there is no difference.  INCOMPATIBILITY.
   1.375 +
   1.376 +* Command "value" now integrates different evaluation mechanisms.  The
   1.377 +result of the first successful evaluation mechanism is printed.  In
   1.378 +square brackets a particular named evaluation mechanisms may be
   1.379 +specified (currently, [SML], [code] or [nbe]).  See further
   1.380 +src/HOL/ex/Eval_Examples.thy.
   1.381 +
   1.382 +* Normalization by evaluation now allows non-leftlinear equations.
   1.383 +Declare with attribute [code nbe].
   1.384 +
   1.385 +* Methods "case_tac" and "induct_tac" now refer to the very same rules
   1.386 +as the structured Isar versions "cases" and "induct", cf. the
   1.387 +corresponding "cases" and "induct" attributes.  Mutual induction rules
   1.388 +are now presented as a list of individual projections
   1.389 +(e.g. foo_bar.inducts for types foo and bar); the old format with
   1.390 +explicit HOL conjunction is no longer supported.  INCOMPATIBILITY, in
   1.391 +rare situations a different rule is selected --- notably nested tuple
   1.392 +elimination instead of former prod.exhaust: use explicit (case_tac t
   1.393 +rule: prod.exhaust) here.
   1.394 +
   1.395 +* Attributes "cases", "induct", "coinduct" support "del" option.
   1.396 +
   1.397 +* Removed fact "case_split_thm", which duplicates "case_split".
   1.398 +
   1.399 +* The option datatype has been moved to a new theory Option.  Renamed
   1.400 +option_map to Option.map, and o2s to Option.set, INCOMPATIBILITY.
   1.401 +
   1.402 +* New predicate "strict_mono" classifies strict functions on partial
   1.403 +orders.  With strict functions on linear orders, reasoning about
   1.404 +(in)equalities is facilitated by theorems "strict_mono_eq",
   1.405 +"strict_mono_less_eq" and "strict_mono_less".
   1.406 +
   1.407 +* Some set operations are now proper qualified constants with
   1.408 +authentic syntax.  INCOMPATIBILITY:
   1.409  
   1.410      op Int ~>   Set.Int
   1.411      op Un ~>    Set.Un
   1.412 @@ -251,26 +306,28 @@
   1.413      {} ~>       Set.empty
   1.414      UNIV ~>     Set.UNIV
   1.415  
   1.416 -* Class complete_lattice with operations Inf, Sup, INFI, SUPR now in theory
   1.417 -Set.
   1.418 -
   1.419 -* Auxiliary class "itself" has disappeared -- classes without any parameter
   1.420 -are treated as expected by the 'class' command.
   1.421 +* Class complete_lattice with operations Inf, Sup, INFI, SUPR now in
   1.422 +theory Set.
   1.423 +
   1.424 +* Auxiliary class "itself" has disappeared -- classes without any
   1.425 +parameter are treated as expected by the 'class' command.
   1.426  
   1.427  * Leibnitz's Series for Pi and the arcus tangens and logarithm series.
   1.428  
   1.429 -* Common decision procedures (Cooper, MIR, Ferrack, Approximation, Dense_Linear_Order)
   1.430 -now in directory HOL/Decision_Procs.
   1.431 -
   1.432 -* Theory HOL/Decision_Procs/Approximation.thy provides the new proof method
   1.433 -"approximation".  It proves formulas on real values by using interval arithmetic.
   1.434 -In the formulas are also the transcendental functions sin, cos, tan, atan, ln,
   1.435 -exp and the constant pi are allowed. For examples see
   1.436 -HOL/Descision_Procs/ex/Approximation_Ex.thy.
   1.437 +* Common decision procedures (Cooper, MIR, Ferrack, Approximation,
   1.438 +Dense_Linear_Order) are now in directory HOL/Decision_Procs.
   1.439 +
   1.440 +* Theory src/HOL/Decision_Procs/Approximation provides the new proof
   1.441 +method "approximation".  It proves formulas on real values by using
   1.442 +interval arithmetic.  In the formulas are also the transcendental
   1.443 +functions sin, cos, tan, atan, ln, exp and the constant pi are
   1.444 +allowed. For examples see
   1.445 +src/HOL/Descision_Procs/ex/Approximation_Ex.thy.
   1.446  
   1.447  * Theory "Reflection" now resides in HOL/Library.
   1.448  
   1.449 -* Entry point to Word library now simply named "Word".  INCOMPATIBILITY.
   1.450 +* Entry point to Word library now simply named "Word".
   1.451 +INCOMPATIBILITY.
   1.452  
   1.453  * Made source layout more coherent with logical distribution
   1.454  structure:
   1.455 @@ -327,82 +384,65 @@
   1.456      src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL
   1.457      src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL
   1.458  
   1.459 -* If methods "eval" and "evaluation" encounter a structured proof state
   1.460 -with !!/==>, only the conclusion is evaluated to True (if possible),
   1.461 -avoiding strange error messages.
   1.462 -
   1.463 -* Simplifier: simproc for let expressions now unfolds if bound variable
   1.464 -occurs at most once in let expression body.  INCOMPATIBILITY.
   1.465 -
   1.466 -* New attribute "arith" for facts that should always be used automaticaly
   1.467 -by arithmetic. It is intended to be used locally in proofs, eg
   1.468 -assumes [arith]: "x > 0"
   1.469 +* If methods "eval" and "evaluation" encounter a structured proof
   1.470 +state with !!/==>, only the conclusion is evaluated to True (if
   1.471 +possible), avoiding strange error messages.
   1.472 +
   1.473 +* Method "sizechange" automates termination proofs using (a
   1.474 +modification of) the size-change principle.  Requires SAT solver.  See
   1.475 +src/HOL/ex/Termination.thy for examples.
   1.476 +
   1.477 +* Simplifier: simproc for let expressions now unfolds if bound
   1.478 +variable occurs at most once in let expression body.  INCOMPATIBILITY.
   1.479 +
   1.480 +* Method "arith": Linear arithmetic now ignores all inequalities when
   1.481 +fast_arith_neq_limit is exceeded, instead of giving up entirely.
   1.482 +
   1.483 +* New attribute "arith" for facts that should always be used
   1.484 +automatically by arithmetic. It is intended to be used locally in
   1.485 +proofs, e.g.
   1.486 +
   1.487 +  assumes [arith]: "x > 0"
   1.488 +
   1.489  Global usage is discouraged because of possible performance impact.
   1.490  
   1.491 -* New classes "top" and "bot" with corresponding operations "top" and "bot"
   1.492 -in theory Orderings;  instantiation of class "complete_lattice" requires
   1.493 -instantiation of classes "top" and "bot".  INCOMPATIBILITY.
   1.494 -
   1.495 -* Changed definition lemma "less_fun_def" in order to provide an instance
   1.496 -for preorders on functions;  use lemma "less_le" instead.  INCOMPATIBILITY.
   1.497 -
   1.498 -* Unified theorem tables for both code code generators.  Thus
   1.499 -[code func] has disappeared and only [code] remains.  INCOMPATIBILITY.
   1.500 -
   1.501 -* Constants "undefined" and "default" replace "arbitrary".  Usually
   1.502 -"undefined" is the right choice to replace "arbitrary", though logically
   1.503 -there is no difference.  INCOMPATIBILITY.
   1.504 -
   1.505 -* Generic ATP manager for Sledgehammer, based on ML threads instead of
   1.506 -Posix processes.  Avoids potentially expensive forking of the ML
   1.507 -process.  New thread-based implementation also works on non-Unix
   1.508 -platforms (Cygwin).  Provers are no longer hardwired, but defined
   1.509 -within the theory via plain ML wrapper functions.  Basic Sledgehammer
   1.510 -commands are covered in the isar-ref manual.
   1.511 -
   1.512 -* Wrapper scripts for remote SystemOnTPTP service allows to use
   1.513 -sledgehammer without local ATP installation (Vampire etc.). Other
   1.514 -provers may be included via suitable ML wrappers, see also
   1.515 -src/HOL/ATP_Linkup.thy.
   1.516 -
   1.517 -* Normalization by evaluation now allows non-leftlinear equations.
   1.518 -Declare with attribute [code nbe].
   1.519 -
   1.520 -* Command "value" now integrates different evaluation
   1.521 -mechanisms.  The result of the first successful evaluation mechanism
   1.522 -is printed.  In square brackets a particular named evaluation
   1.523 -mechanisms may be specified (currently, [SML], [code] or [nbe]).  See
   1.524 -further src/HOL/ex/Eval_Examples.thy.
   1.525 -
   1.526 -* New method "sizechange" to automate termination proofs using (a
   1.527 -modification of) the size-change principle. Requires SAT solver. See
   1.528 -src/HOL/ex/Termination.thy for examples.
   1.529 -
   1.530 -* HOL/Orderings: class "wellorder" moved here, with explicit induction
   1.531 -rule "less_induct" as assumption.  For instantiation of "wellorder" by
   1.532 -means of predicate "wf", use rule wf_wellorderI.  INCOMPATIBILITY.
   1.533 -
   1.534 -* HOL/Orderings: added class "preorder" as superclass of "order".
   1.535 +* New classes "top" and "bot" with corresponding operations "top" and
   1.536 +"bot" in theory Orderings; instantiation of class "complete_lattice"
   1.537 +requires instantiation of classes "top" and "bot".  INCOMPATIBILITY.
   1.538 +
   1.539 +* Changed definition lemma "less_fun_def" in order to provide an
   1.540 +instance for preorders on functions; use lemma "less_le" instead.
   1.541 +INCOMPATIBILITY.
   1.542 +
   1.543 +* Theory Orderings: class "wellorder" moved here, with explicit
   1.544 +induction rule "less_induct" as assumption.  For instantiation of
   1.545 +"wellorder" by means of predicate "wf", use rule wf_wellorderI.
   1.546 +INCOMPATIBILITY.
   1.547 +
   1.548 +* Theory Orderings: added class "preorder" as superclass of "order".
   1.549  INCOMPATIBILITY: Instantiation proofs for order, linorder
   1.550  etc. slightly changed.  Some theorems named order_class.* now named
   1.551  preorder_class.*.
   1.552  
   1.553 -* HOL/Relation:
   1.554 -Renamed "refl" to "refl_on", "reflexive" to "refl, "diag" to "Id_on".
   1.555 -
   1.556 -* HOL/Finite_Set: added a new fold combinator of type
   1.557 +* Theory Relation: renamed "refl" to "refl_on", "reflexive" to "refl,
   1.558 +"diag" to "Id_on".
   1.559 +
   1.560 +* Theory Finite_Set: added a new fold combinator of type
   1.561 +
   1.562    ('a => 'b => 'b) => 'b => 'a set => 'b
   1.563 -Occasionally this is more convenient than the old fold combinator which is
   1.564 -now defined in terms of the new one and renamed to fold_image.
   1.565 -
   1.566 -* HOL/Ring_and_Field and HOL/OrderedGroup: The lemmas "group_simps" and
   1.567 -"ring_simps" have been replaced by "algebra_simps" (which can be extended with
   1.568 -further lemmas!). At the moment both still exist but the former will disappear
   1.569 -at some point.
   1.570 -
   1.571 -* HOL/Power: Lemma power_Suc is now declared as a simp rule in class
   1.572 -recpower.  Type-specific simp rules for various recpower types have
   1.573 -been removed.  INCOMPATIBILITY.  Rename old lemmas as follows:
   1.574 +
   1.575 +Occasionally this is more convenient than the old fold combinator
   1.576 +which is now defined in terms of the new one and renamed to
   1.577 +fold_image.
   1.578 +
   1.579 +* Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps"
   1.580 +and "ring_simps" have been replaced by "algebra_simps" (which can be
   1.581 +extended with further lemmas!).  At the moment both still exist but
   1.582 +the former will disappear at some point.
   1.583 +
   1.584 +* Theory Power: Lemma power_Suc is now declared as a simp rule in
   1.585 +class recpower.  Type-specific simp rules for various recpower types
   1.586 +have been removed.  INCOMPATIBILITY, rename old lemmas as follows:
   1.587  
   1.588  rat_power_0    -> power_0
   1.589  rat_power_Suc  -> power_Suc
   1.590 @@ -413,7 +453,7 @@
   1.591  power_poly_0   -> power_0
   1.592  power_poly_Suc -> power_Suc
   1.593  
   1.594 -* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been
   1.595 +* Theories Ring_and_Field and Divides: Definition of "op dvd" has been
   1.596  moved to separate class dvd in Ring_and_Field; a couple of lemmas on
   1.597  dvd has been generalized to class comm_semiring_1.  Likewise a bunch
   1.598  of lemmas from Divides has been generalized from nat to class
   1.599 @@ -428,9 +468,9 @@
   1.600      mult_div ~>             div_mult_self2_is_id
   1.601      mult_mod ~>             mod_mult_self2_is_0
   1.602  
   1.603 -* HOL/IntDiv: removed many lemmas that are instances of class-based
   1.604 -generalizations (from Divides and Ring_and_Field).
   1.605 -INCOMPATIBILITY. Rename old lemmas as follows:
   1.606 +* Theory IntDiv: removed many lemmas that are instances of class-based
   1.607 +generalizations (from Divides and Ring_and_Field).  INCOMPATIBILITY,
   1.608 +rename old lemmas as follows:
   1.609  
   1.610  dvd_diff               -> nat_dvd_diff
   1.611  dvd_zminus_iff         -> dvd_minus_iff
   1.612 @@ -478,11 +518,38 @@
   1.613  zdvd_1_left            -> one_dvd
   1.614  zminus_dvd_iff         -> minus_dvd_iff
   1.615  
   1.616 -* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
   1.617 +* Theory Rational: 'Fract k 0' now equals '0'.  INCOMPATIBILITY.
   1.618 +
   1.619 +* The real numbers offer decimal input syntax: 12.34 is translated
   1.620 +into 1234/10^2. This translation is not reversed upon output.
   1.621 +
   1.622 +* Theory Library/Polynomial defines an abstract type 'a poly of
   1.623 +univariate polynomials with coefficients of type 'a.  In addition to
   1.624 +the standard ring operations, it also supports div and mod.  Code
   1.625 +generation is also supported, using list-style constructors.
   1.626 +
   1.627 +* Theory Library/Inner_Product defines a class of real_inner for real
   1.628 +inner product spaces, with an overloaded operation inner :: 'a => 'a
   1.629 +=> real.  Class real_inner is a subclass of real_normed_vector from
   1.630 +theory RealVector.
   1.631 +
   1.632 +* Theory Library/Product_Vector provides instances for the product
   1.633 +type 'a * 'b of several classes from RealVector and Inner_Product.
   1.634 +Definitions of addition, subtraction, scalar multiplication, norms,
   1.635 +and inner products are included.
   1.636 +
   1.637 +* Theory Library/Bit defines the field "bit" of integers modulo 2.  In
   1.638 +addition to the field operations, numerals and case syntax are also
   1.639 +supported.
   1.640 +
   1.641 +* Theory Library/Diagonalize provides constructive version of Cantor's
   1.642 +first diagonalization argument.
   1.643 +
   1.644 +* Theory Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
   1.645  zlcm (for int); carried together from various gcd/lcm developements in
   1.646 -the HOL Distribution.  zgcd and zlcm replace former igcd and ilcm;
   1.647 -corresponding theorems renamed accordingly.  INCOMPATIBILITY.  To
   1.648 -recover tupled syntax, use syntax declarations like:
   1.649 +the HOL Distribution.  Constants zgcd and zlcm replace former igcd and
   1.650 +ilcm; corresponding theorems renamed accordingly.  INCOMPATIBILITY,
   1.651 +may recover tupled syntax as follows:
   1.652  
   1.653      hide (open) const gcd
   1.654      abbreviation gcd where
   1.655 @@ -490,54 +557,24 @@
   1.656      notation (output)
   1.657        GCD.gcd ("gcd '(_, _')")
   1.658  
   1.659 -(analogously for lcm, zgcd, zlcm).
   1.660 -
   1.661 -* HOL/Real/Rational: 'Fract k 0' now equals '0'.  INCOMPATIBILITY.
   1.662 -
   1.663 -* The real numbers offer decimal input syntax: 12.34 is translated into
   1.664 -  1234/10^2. This translation is not reversed upon output.
   1.665 -
   1.666 -* New ML antiquotation @{code}: takes constant as argument, generates
   1.667 +The same works for lcm, zgcd, zlcm.
   1.668 +
   1.669 +* Theory Library/Nat_Infinity: added addition, numeral syntax and more
   1.670 +instantiations for algebraic structures.  Removed some duplicate
   1.671 +theorems.  Changes in simp rules.  INCOMPATIBILITY.
   1.672 +
   1.673 +* ML antiquotation @{code} takes a constant as argument and generates
   1.674  corresponding code in background and inserts name of the corresponding
   1.675  resulting ML value/function/datatype constructor binding in place.
   1.676  All occurrences of @{code} with a single ML block are generated
   1.677  simultaneously.  Provides a generic and safe interface for
   1.678 -instrumentalizing code generation.  See HOL/Decision_Procs/Ferrack for
   1.679 -a more ambitious application.  In future you ought refrain from ad-hoc
   1.680 -compiling generated SML code on the ML toplevel.  Note that (for technical
   1.681 -reasons) @{code} cannot refer to constants for which user-defined
   1.682 -serializations are set.  Refer to the corresponding ML counterpart
   1.683 -directly in that cases.
   1.684 -
   1.685 -* Integrated image HOL-Complex with HOL.  Entry points Main.thy and
   1.686 -Complex_Main.thy remain as they are.
   1.687 -
   1.688 -* New image HOL-Plain provides a minimal HOL with the most important
   1.689 -tools available (inductive, datatype, primrec, ...).  By convention
   1.690 -the corresponding theory Plain should be ancestor of every further
   1.691 -(library) theory.  Some library theories now have ancestor Plain
   1.692 -(instead of Main), thus theory Main occasionally has to be imported
   1.693 -explicitly.
   1.694 -
   1.695 -* The metis method now fails in the usual manner, rather than raising
   1.696 -an exception, if it determines that it cannot prove the theorem.
   1.697 -
   1.698 -* The metis method no longer fails because the theorem is too trivial
   1.699 -(contains the empty clause).
   1.700 -
   1.701 -* Methods "case_tac" and "induct_tac" now refer to the very same rules
   1.702 -as the structured Isar versions "cases" and "induct", cf. the
   1.703 -corresponding "cases" and "induct" attributes.  Mutual induction rules
   1.704 -are now presented as a list of individual projections
   1.705 -(e.g. foo_bar.inducts for types foo and bar); the old format with
   1.706 -explicit HOL conjunction is no longer supported.  INCOMPATIBILITY, in
   1.707 -rare situations a different rule is selected --- notably nested tuple
   1.708 -elimination instead of former prod.exhaust: use explicit (case_tac t
   1.709 -rule: prod.exhaust) here.
   1.710 -
   1.711 -* Attributes "cases", "induct", "coinduct" support "del" option.
   1.712 -
   1.713 -* Removed fact "case_split_thm", which duplicates "case_split".
   1.714 +instrumentalizing code generation.  See
   1.715 +src/HOL/Decision_Procs/Ferrack.thy for a more ambitious application.
   1.716 +In future you ought to refrain from ad-hoc compiling generated SML
   1.717 +code on the ML toplevel.  Note that (for technical reasons) @{code}
   1.718 +cannot refer to constants for which user-defined serializations are
   1.719 +set.  Refer to the corresponding ML counterpart directly in that
   1.720 +cases.
   1.721  
   1.722  * Command 'rep_datatype': instead of theorem names the command now
   1.723  takes a list of terms denoting the constructors of the type to be
   1.724 @@ -551,19 +588,6 @@
   1.725      Suc_Suc_eq                  ~> nat.inject
   1.726      Suc_not_Zero Zero_not_Suc   ~> nat.distinct
   1.727  
   1.728 -* The option datatype has been moved to a new theory HOL/Option.thy.
   1.729 -Renamed option_map to Option.map, and o2s to Option.set.
   1.730 -
   1.731 -* Library/Nat_Infinity: added addition, numeral syntax and more
   1.732 -instantiations for algebraic structures.  Removed some duplicate
   1.733 -theorems.  Changes in simp rules.  INCOMPATIBILITY.
   1.734 -
   1.735 -* ATP selection (E/Vampire/Spass) is now via Proof General's settings
   1.736 -menu.
   1.737 -
   1.738 -* Linear arithmetic now ignores all inequalities when
   1.739 -fast_arith_neq_limit is exceeded, instead of giving up entirely.
   1.740 -
   1.741  
   1.742  *** HOL-Algebra ***
   1.743  
   1.744 @@ -573,11 +597,12 @@
   1.745  
   1.746  * New theory of factorial domains.
   1.747  
   1.748 -* Units_l_inv and Units_r_inv are now simprules by default.
   1.749 +* Units_l_inv and Units_r_inv are now simp rules by default.
   1.750  INCOMPATIBILITY.  Simplifier proof that require deletion of l_inv
   1.751  and/or r_inv will now also require deletion of these lemmas.
   1.752  
   1.753 -* Renamed the following theorems.  INCOMPATIBILITY.
   1.754 +* Renamed the following theorems, INCOMPATIBILITY:
   1.755 +
   1.756  UpperD ~> Upper_memD
   1.757  LowerD ~> Lower_memD
   1.758  least_carrier ~> least_closed
   1.759 @@ -587,19 +612,6 @@
   1.760  one_not_zero ~> carrier_one_not_zero  (collision with assumption)
   1.761  
   1.762  
   1.763 -*** HOL-NSA ***
   1.764 -
   1.765 -* Created new image HOL-NSA, containing theories of nonstandard
   1.766 -analysis which were previously part of HOL-Complex.  Entry point
   1.767 -Hyperreal.thy remains valid, but theories formerly using
   1.768 -Complex_Main.thy should now use new entry point Hypercomplex.thy.
   1.769 -
   1.770 -
   1.771 -*** ZF ***
   1.772 -
   1.773 -* Proof of Zorn's Lemma for partial orders.
   1.774 -
   1.775 -
   1.776  *** HOLCF ***
   1.777  
   1.778  * Reimplemented the simplification procedure for proving continuity
   1.779 @@ -612,23 +624,47 @@
   1.780  old one could solve, and "simp add: cont2cont_LAM" may be necessary.
   1.781  Potential INCOMPATIBILITY.
   1.782  
   1.783 -* The syntax of the fixrec package has changed.  The specification
   1.784 -syntax now conforms in style to definition, primrec, function, etc.
   1.785 -See HOLCF/ex/Fixrec_ex.thy for examples.  INCOMPATIBILITY.
   1.786 +* The syntax of the fixrec package now conforms to the general
   1.787 +specification format of inductive, primrec, function, etc.  See
   1.788 +src/HOLCF/ex/Fixrec_ex.thy for examples.  INCOMPATIBILITY.
   1.789 +
   1.790 +
   1.791 +*** ZF ***
   1.792 +
   1.793 +* Proof of Zorn's Lemma for partial orders.
   1.794  
   1.795  
   1.796  *** ML ***
   1.797  
   1.798 +* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for
   1.799 +Poly/ML 5.2.1 or later.  Important note: the TimeLimit facility
   1.800 +depends on multithreading, so timouts will not work before Poly/ML
   1.801 +5.2.1!
   1.802 +
   1.803  * High-level support for concurrent ML programming, see
   1.804  src/Pure/Cuncurrent.  The data-oriented model of "future values" is
   1.805  particularly convenient to organize independent functional
   1.806  computations.  The concept of "synchronized variables" provides a
   1.807  higher-order interface for components with shared state, avoiding the
   1.808 -delicate details of mutexes and condition variables.  [Poly/ML 5.2.1
   1.809 -or later]
   1.810 +delicate details of mutexes and condition variables.  (Requires
   1.811 +Poly/ML 5.2.1 or later.)
   1.812 +
   1.813 +* ML bindings produced via Isar commands are stored within the Isar
   1.814 +context (theory or proof).  Consequently, commands like 'use' and 'ML'
   1.815 +become thread-safe and work with undo as expected (concerning
   1.816 +top-level bindings, not side-effects on global references).
   1.817 +INCOMPATIBILITY, need to provide proper Isar context when invoking the
   1.818 +compiler at runtime; really global bindings need to be given outside a
   1.819 +theory.  (Requires Poly/ML 5.2 or later.)
   1.820 +
   1.821 +* Command 'ML_prf' is analogous to 'ML' but works within a proof
   1.822 +context.  Top-level ML bindings are stored within the proof context in
   1.823 +a purely sequential fashion, disregarding the nested proof structure.
   1.824 +ML bindings introduced by 'ML_prf' are discarded at the end of the
   1.825 +proof.  (Requires Poly/ML 5.2 or later.)
   1.826  
   1.827  * Simplified ML attribute and method setup, cf. functions Attrib.setup
   1.828 -and Method.setup, as well as commands 'attribute_setup' and
   1.829 +and Method.setup, as well as Isar commands 'attribute_setup' and
   1.830  'method_setup'.  INCOMPATIBILITY for 'method_setup', need to simplify
   1.831  existing code accordingly, or use plain 'setup' together with old
   1.832  Method.add_method.
   1.833 @@ -640,52 +676,27 @@
   1.834  accordingly.  Note that extra performance may be gained by producing
   1.835  the cterm carefully, avoiding slow Thm.cterm_of.
   1.836  
   1.837 -* ML bindings produced via Isar commands are stored within the Isar
   1.838 -context (theory or proof).  Consequently, commands like 'use' and 'ML'
   1.839 -become thread-safe and work with undo as expected (concerning
   1.840 -top-level bindings, not side-effects on global references).
   1.841 -INCOMPATIBILITY, need to provide proper Isar context when invoking the
   1.842 -compiler at runtime; really global bindings need to be given outside a
   1.843 -theory. [Poly/ML 5.2 or later]
   1.844 -
   1.845 -* Command 'ML_prf' is analogous to 'ML' but works within a proof
   1.846 -context. Top-level ML bindings are stored within the proof context in
   1.847 -a purely sequential fashion, disregarding the nested proof structure.
   1.848 -ML bindings introduced by 'ML_prf' are discarded at the end of the
   1.849 -proof.  [Poly/ML 5.2 or later]
   1.850 -
   1.851 -* Generic Toplevel.add_hook interface allows to analyze the result of
   1.852 -transactions.  E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML
   1.853 -for theorem dependency output of transactions resulting in a new
   1.854 -theory state.
   1.855 +* Simplified interface for defining document antiquotations via
   1.856 +ThyOutput.antiquotation, ThyOutput.output, and optionally
   1.857 +ThyOutput.maybe_pretty_source.  INCOMPATIBILITY, need to simplify user
   1.858 +antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common
   1.859 +examples.
   1.860  
   1.861  * More systematic treatment of long names, abstract name bindings, and
   1.862  name space operations.  Basic operations on qualified names have been
   1.863  move from structure NameSpace to Long_Name, e.g. Long_Name.base_name,
   1.864  Long_Name.append.  Old type bstring has been mostly replaced by
   1.865  abstract type binding (see structure Binding), which supports precise
   1.866 -qualification (by packages and local theory targets), as well as
   1.867 -proper tracking of source positions.  INCOMPATIBILITY, need to wrap
   1.868 -old bstring values into Binding.name, or better pass through abstract
   1.869 +qualification by packages and local theory targets, as well as proper
   1.870 +tracking of source positions.  INCOMPATIBILITY, need to wrap old
   1.871 +bstring values into Binding.name, or better pass through abstract
   1.872  bindings everywhere.  See further src/Pure/General/long_name.ML,
   1.873  src/Pure/General/binding.ML and src/Pure/General/name_space.ML
   1.874  
   1.875 -* Simplified interface for defining document antiquotations via
   1.876 -ThyOutput.antiquotation, ThyOutput.output, and optionally
   1.877 -ThyOutput.maybe_pretty_source.  INCOMPATIBILITY, need to simplify user
   1.878 -antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common
   1.879 -examples.
   1.880 -
   1.881  * Result facts (from PureThy.note_thms, ProofContext.note_thms,
   1.882  LocalTheory.note etc.) now refer to the *full* internal name, not the
   1.883  bstring as before.  INCOMPATIBILITY, not detected by ML type-checking!
   1.884  
   1.885 -* Rules and tactics that read instantiations (read_instantiate,
   1.886 -res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
   1.887 -context, which is required for parsing and type-checking.  Moreover,
   1.888 -the variables are specified as plain indexnames, not string encodings
   1.889 -thereof.  INCOMPATIBILITY.
   1.890 -
   1.891  * Disposed old type and term read functions (Sign.read_def_typ,
   1.892  Sign.read_typ, Sign.read_def_terms, Sign.read_term,
   1.893  Thm.read_def_cterms, Thm.read_cterm etc.).  INCOMPATIBILITY, should
   1.894 @@ -699,9 +710,21 @@
   1.895  embedded ML text, or local_simpset_of with a proper context passed as
   1.896  explicit runtime argument.
   1.897  
   1.898 -* Antiquotations: block-structured compilation context indicated by
   1.899 +* Rules and tactics that read instantiations (read_instantiate,
   1.900 +res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
   1.901 +context, which is required for parsing and type-checking.  Moreover,
   1.902 +the variables are specified as plain indexnames, not string encodings
   1.903 +thereof.  INCOMPATIBILITY.
   1.904 +
   1.905 +* Generic Toplevel.add_hook interface allows to analyze the result of
   1.906 +transactions.  E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML
   1.907 +for theorem dependency output of transactions resulting in a new
   1.908 +theory state.
   1.909 +
   1.910 +* ML antiquotations: block-structured compilation context indicated by
   1.911  \<lbrace> ... \<rbrace>; additional antiquotation forms:
   1.912  
   1.913 +  @{binding name}                         - basic name binding
   1.914    @{let ?pat = term}                      - term abbreviation (HO matching)
   1.915    @{note name = fact}                     - fact abbreviation
   1.916    @{thm fact}                             - singleton fact (with attributes)
   1.917 @@ -715,9 +738,6 @@
   1.918  
   1.919  *** System ***
   1.920  
   1.921 -* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for
   1.922 -Poly/ML 5.2.1 or later.
   1.923 -
   1.924  * The Isabelle "emacs" tool provides a specific interface to invoke
   1.925  Proof General / Emacs, with more explicit failure if that is not
   1.926  installed (the old isabelle-interface script silently falls back on
   1.927 @@ -729,13 +749,13 @@
   1.928  Isabelle/lib/jedit/plugin for a minimal example.  (The obsolete Java
   1.929  process wrapper has been discontinued.)
   1.930  
   1.931 -* Status messages (with exact source position information) are
   1.932 +* Added homegrown Isabelle font with unicode layout, see lib/fonts.
   1.933 +
   1.934 +* Various status messages (with exact source position information) are
   1.935  emitted, if proper markup print mode is enabled.  This allows
   1.936  user-interface components to provide detailed feedback on internal
   1.937  prover operations.
   1.938  
   1.939 -* Homegrown Isabelle font with unicode layout, see Isabelle/lib/fonts.
   1.940 -
   1.941  
   1.942  
   1.943  New in Isabelle2008 (June 2008)