NEWS

 New in this Isabelle release
 ----------------------------
 
 *** General ***
 
-* The type Library.option is no more, along with the exception
+* ML: The type Library.option is no more, along with the exception
   Library.OPTION: Isabelle now uses the standard option type.  The
   functions the, is_some, is_none, etc. are still in Library, but
   the constructors are now SOME and NONE instead of Some and None.
-  They throw the exception Option.
-
-* The exception LIST is no more, the standard exceptions Empty and
+  They raise the exception Option.
+
+* ML: The exception LIST is no more, the standard exceptions Empty and
   Subscript, as well as Library.UnequalLengths are used instead.  This
   means that function like Library.hd and Library.tl are gone, as the
   standard hd and tl functions suffice.
 
   A number of functions, specifically those in the LIBRARY_CLOSED

   from the standard).
 
   A simple solution to broken code is to include "open Library" at the
   beginning of a structure.  Everything after that will be as before.
 
-* Document preparation: new antiquotations @{lhs thm} and @{rhs thm}
-  printing the lhs/rhs of definitions, equations, inequations etc. 
-
-* isatool usedir: new option -f that allows specification of the ML
-  file to be used by Isabelle; default is ROOT.ML.
-
 * Theory headers: the new header syntax for Isar theories is
 
   theory <name>
   imports <theory1> ... <theoryn>
   begin

   simprocs is gone -- use prems_of_ss on the simpset instead.
   Moreover, the low-level mk_simproc no longer applies Logic.varify
   internally, to allow for use in a context of fixed variables.
 
 * Pure/Simplifier: Command "find_rewrites" takes a string and lists all
-  equality theorems (not just those with attribute simp!) whose left-hand
+  equality theorems (not just those declared as simp!) whose left-hand
   side matches the term given via the string. In PG the command can be
   activated via Isabelle -> Show me -> matching rewrites.
 
-* Provers: Simplifier and Classical Reasoner now support proof context
-  dependent plug-ins (simprocs, solvers, wrappers etc.).  These extra
-  components are stored in the theory and patched into the
-  simpset/claset when used in an Isar proof context.  Context
-  dependent components are maintained by the following theory
-  operations:
-
-    Simplifier.add_context_simprocs
-    Simplifier.del_context_simprocs
-    Simplifier.set_context_subgoaler
-    Simplifier.reset_context_subgoaler
-    Simplifier.add_context_looper
-    Simplifier.del_context_looper
-    Simplifier.add_context_unsafe_solver
-    Simplifier.add_context_safe_solver
-
-    Classical.add_context_safe_wrapper
-    Classical.del_context_safe_wrapper
-    Classical.add_context_unsafe_wrapper
-    Classical.del_context_unsafe_wrapper
-
-  IMPORTANT NOTE: proof tools (methods etc.) need to use
-  local_simpset_of and local_claset_of to instead of the primitive
-  Simplifier.get_local_simpset and Classical.get_local_claset,
-  respectively, in order to see the context dependent fields!
-
-* Document preparation: antiquotations now provide the option
-  'locale=NAME' to specify an alternative context used for evaluating
-  and printing the subsequent argument, as in @{thm [locale=LC]
-  fold_commute}, for example.
-
-* Document preparation: commands 'display_drafts' and 'print_drafts'
-  perform simple output of raw sources.  Only those symbols that do
-  not require additional LaTeX packages (depending on comments in
-  isabellesym.sty) are displayed properly, everything else is left
-  verbatim.  We use isatool display and isatool print as front ends;
-  these are subject to the DVI_VIEWER and PRINT_COMMAND settings,
-  respectively.
-
-* Document preparation: Proof scripts as well as some other commands
-  such as ML or parse/print_translation can now be hidden in the document.
-  Hiding is enabled by default, and can be disabled either via the option
-  '-H false' of isatool usedir or by resetting the reference variable
+* Isar debugging: new reference Toplevel.debug; default false.
+  Set to make printing of exceptions THM, TERM, TYPE and THEORY more verbose.
+  
+* Locales:
+  - "includes" disallowed in declaration of named locales (command "locale").
+  - Fixed parameter management in theorem generation for goals with "includes".
+    INCOMPATIBILITY: rarely, the generated theorem statement is different.
+
+* Locales:  new commands for the interpretation of locale expressions
+  in theories (interpretation) and proof contexts (interpret).  These take an
+  instantiation of the locale parameters and compute proof obligations from
+  the instantiated specification.  After the obligations have been discharged,
+  the instantiated theorems of the locale are added to the theory or proof
+  context.  Interpretation is smart in that already active interpretations
+  do not occur in proof obligations, neither are instantiated theorems stored
+  in duplicate.
+  Use print_interps to inspect active interpretations of a particular locale.
+
+* Isar: new syntax 'name(i-j, i-, i, ...)' for referring to specific
+  selections of theorems in named facts via indices.
+
+
+*** Document preparation ***
+
+* New antiquotations @{lhs thm} and @{rhs thm} printing the lhs/rhs of
+  definitions, equations, inequations etc.
+
+* Antiquotations now provide the option 'locale=NAME' to specify an
+  alternative context used for evaluating and printing the subsequent
+  argument, as in @{thm [locale=LC] fold_commute}, for example.
+
+* Commands 'display_drafts' and 'print_drafts' perform simple output
+  of raw sources.  Only those symbols that do not require additional
+  LaTeX packages (depending on comments in isabellesym.sty) are
+  displayed properly, everything else is left verbatim.  We use
+  isatool display and isatool print as front ends; these are subject
+  to the DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively.
+
+* Proof scripts as well as some other commands such as ML or
+  parse/print_translation can now be hidden in the document.  Hiding
+  is enabled by default, and can be disabled either via the option '-H
+  false' of isatool usedir or by resetting the reference variable
   IsarOutput.hide_commands. Additional commands to be hidden may be
   declared using IsarOutput.add_hidden_commands.
 
-* ML: output via the Isabelle channels of writeln/warning/error
+
+*** HOL ***
+
+* Datatype induction via method `induct' now preserves the name of the
+  induction variable. For example, when proving P(xs::'a list) by induction
+  on xs, the induction step is now P(xs) ==> P(a#xs) rather than
+  P(list) ==> P(a#list) as previously.
+
+* HOL/record: reimplementation of records. Improved scalability for
+  records with many fields, avoiding performance problems for type
+  inference. Records are no longer composed of nested field types, but
+  of nested extension types. Therefore the record type only grows
+  linear in the number of extensions and not in the number of fields.
+  The top-level (users) view on records is preserved.  Potential
+  INCOMPATIBILITY only in strange cases, where the theory depends on
+  the old record representation. The type generated for a record is
+  called <record_name>_ext_type.
+
+* HOL/record: Reference record_quick_and_dirty_sensitive can be
+  enabled to skip the proofs triggered by a record definition or a
+  simproc (if quick_and_dirty is enabled). Definitions of large
+  records can take quite long.
+
+* HOL/record: "record_upd_simproc" for simplification of multiple
+  record updates enabled by default.  Moreover, trivial updates are
+  also removed: r(|x := x r|) = r.  INCOMPATIBILITY: old proofs break
+  occasionally, since simplification is more powerful by default.
+
+* HOL: symbolic syntax of Hilbert Choice Operator is now as follows:
+
+  syntax (epsilon)
+    "_Eps" :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
+
+  The symbol \<some> is displayed as the alternative epsilon of LaTeX
+  and x-symbol; use option '-m epsilon' to get it actually printed.
+  Moreover, the mathematically important symbolic identifier
+  \<epsilon> becomes available as variable, constant etc.
+
+* HOL: "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
+  Similarly for all quantifiers: "ALL x > y" etc.
+  The x-symbol for >= is \<ge>.
+
+* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}"
+           (and similarly for "\<in>" instead of ":")
+
+* HOL/SetInterval: The syntax for open intervals has changed:
+
+  Old         New
+  {..n(}   -> {..<n}
+  {)n..}   -> {n<..}
+  {m..n(}  -> {m..<n}
+  {)m..n}  -> {m<..n}
+  {)m..n(} -> {m<..<n}
+
+  The old syntax is still supported but will disappear in the future.
+  For conversion use the following emacs search and replace patterns:
+
+  {)\([^\.]*\)\.\.  ->  {\1<\.\.}
+  \.\.\([^(}]*\)(}  ->  \.\.<\1}
+
+  They are not perfect but work quite well.
+
+* HOL: The syntax for 'setsum', summation over finite sets, has changed:
+
+  The syntax for 'setsum (%x. e) A' used to be '\<Sum>x:A. e'
+  and is now either 'SUM x:A. e' or '\<Sum>x\<in>A. e'.
+
+  There is new syntax for summation over finite sets:
+
+  '\<Sum>x | P. e'    is the same as  'setsum (%x. e) {x. P}'
+  '\<Sum>x=a..b. e'   is the same as  'setsum (%x. e) {a..b}'
+  '\<Sum>x=a..<b. e'  is the same as  'setsum (%x. e) {a..<b}'
+  '\<Sum>x<k. e'      is the same as  'setsum (%x. e) {..<k}'
+
+  Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e'
+  now translates into 'setsum' as above.
+
+* HOL: Finite set induction: In Isar proofs, the insert case is now
+  "case (insert x F)" instead of the old counterintuitive "case (insert F x)".
+
+* HOL/Simplifier:
+
+  - Is now set up to reason about transitivity chains involving "trancl"
+  (r^+) and "rtrancl" (r^*) by setting up tactics provided by
+  Provers/trancl.ML as additional solvers.  INCOMPATIBILITY: old proofs break
+  occasionally as simplification may now solve more goals than previously.
+
+  - Converts x <= y into x = y if assumption y <= x is present.  Works for
+  all partial orders (class "order"), in particular numbers and sets. For
+  linear orders (e.g. numbers) it treats ~ x < y just like y <= x.
+
+  - Simproc for "let x = a in f x"
+  If a is a free or bound variable or a constant then the let is unfolded.
+  Otherwise first a is simplified to a', and then f a' is simplified to
+  g. If possible we abstract a' from g arriving at "let x = a' in g' x",
+  otherwise we unfold the let and arrive at g. The simproc can be 
+  enabled/disabled by the reference use_let_simproc. Potential
+  INCOMPATIBILITY since simplification is more powerful by default.
+ 
+
+*** HOLCF ***
+
+* HOLCF: discontinued special version of 'constdefs' (which used to
+  support continuous functions) in favor of the general Pure one with
+  full type-inference.
+
+
+*** ZF ***
+
+* ZF/ex/{Group,Ring}: examples in abstract algebra, including the
+  First Isomorphism Theorem (on quotienting by the kernel of a
+  homomorphism).
+
+* ZF/Simplifier: install second copy of type solver that actually
+  makes use of TC rules declared to Isar proof contexts (or locales);
+  the old version is still required for ML proof scripts.
+
+
+*** System ***
+
+* HOL: isatool dimacs2hol converts files in DIMACS CNF format
+  (containing Boolean satisfiability problems) into Isabelle/HOL
+  theories.
+
+* isatool usedir: option -f allows specification of the ML file to be
+  used by Isabelle; default is ROOT.ML.
+
+* ISABELLE_DOC_FORMAT setting specifies preferred document format (for
+  isatool doc, isatool mkdir, display_drafts etc.).
+
+
+*** ML ***
+
+* Pure: output via the Isabelle channels of writeln/warning/error
   etc. is now passed through Output.output, with a hook for arbitrary
   transformations depending on the print_mode (cf. Output.add_mode --
   the first active mode that provides a output function wins).
   Already formatted output may be embedded into further text via
   Output.raw; the result of Pretty.string_of/str_of and derived

   translations to produce properly formatted results; Output.raw is
   required when capturing already output material that will eventually
   be presented to the user a second time.  For the default print mode,
   both Output.output and Output.raw have no effect.
 
-
-*** Isar ***
-
-* Debugging: new reference Toplevel.debug; default false.
-  Set to make printing of exceptions THM, TERM, TYPE and THEORY more verbose.
-  
-* Locales:
-  - "includes" disallowed in declaration of named locales (command "locale").
-  - Fixed parameter management in theorem generation for goals with "includes".
-    INCOMPATIBILITY: rarely, the generated theorem statement is different.
-
-* Locales:  new commands for the interpretation of locale expressions
-  in theories (interpretation) and proof contexts (interpret).  These take an
-  instantiation of the locale parameters and compute proof obligations from
-  the instantiated specification.  After the obligations have been discharged,
-  the instantiated theorems of the locale are added to the theory or proof
-  context.  Interpretation is smart in that already active interpretations
-  do not occur in proof obligations, neither are instantiated theorems stored
-  in duplicate.
-  Use print_interps to inspect active interpretations of a particular locale.
-
-* New syntax
-
-    <theorem_name> (<index>, ..., <index>-<index>, ...)
-
-  for referring to specific theorems in a named list of theorems via
-  indices.
-
-*** HOL ***
-
-* Datatype induction via method `induct' now preserves the name of the
-  induction variable. For example, when proving P(xs::'a list) by induction
-  on xs, the induction step is now P(xs) ==> P(a#xs) rather than
-  P(list) ==> P(a#list) as previously.
-
-* HOL/record: reimplementation of records. Improved scalability for
-  records with many fields, avoiding performance problems for type
-  inference. Records are no longer composed of nested field types, but
-  of nested extension types. Therefore the record type only grows
-  linear in the number of extensions and not in the number of fields.
-  The top-level (users) view on records is preserved.  Potential
-  INCOMPATIBILITY only in strange cases, where the theory depends on
-  the old record representation. The type generated for a record is
-  called <record_name>_ext_type.
-
-* HOL/record: Reference record_quick_and_dirty_sensitive can be
-  enabled to skip the proofs triggered by a record definition or a
-  simproc (if quick_and_dirty is enabled). Definitions of large
-  records can take quite long.
-
-* HOL/record: "record_upd_simproc" for simplification of multiple
-  record updates enabled by default.  Moreover, trivial updates are
-  also removed: r(|x := x r|) = r.  INCOMPATIBILITY: old proofs break
-  occasionally, since simplification is more powerful by default.
-
-* HOL: symbolic syntax of Hilbert Choice Operator is now as follows:
-
-  syntax (epsilon)
-    "_Eps" :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
-
-  The symbol \<some> is displayed as the alternative epsilon of LaTeX
-  and x-symbol; use option '-m epsilon' to get it actually printed.
-  Moreover, the mathematically important symbolic identifier
-  \<epsilon> becomes available as variable, constant etc.
-
-* HOL: "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
-  Similarly for all quantifiers: "ALL x > y" etc.
-  The x-symbol for >= is \<ge>.
-
-* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}"
-           (and similarly for "\<in>" instead of ":")
-
-* HOL/SetInterval: The syntax for open intervals has changed:
-
-  Old         New
-  {..n(}   -> {..<n}
-  {)n..}   -> {n<..}
-  {m..n(}  -> {m..<n}
-  {)m..n}  -> {m<..n}
-  {)m..n(} -> {m<..<n}
-
-  The old syntax is still supported but will disappear in the future.
-  For conversion use the following emacs search and replace patterns:
-
-  {)\([^\.]*\)\.\.  ->  {\1<\.\.}
-  \.\.\([^(}]*\)(}  ->  \.\.<\1}
-
-  They are not perfect but work quite well.
-
-* HOL: The syntax for 'setsum', summation over finite sets, has changed:
-
-  The syntax for 'setsum (%x. e) A' used to be '\<Sum>x:A. e'
-  and is now either 'SUM x:A. e' or '\<Sum>x\<in>A. e'.
-
-  There is new syntax for summation over finite sets:
-
-  '\<Sum>x | P. e'    is the same as  'setsum (%x. e) {x. P}'
-  '\<Sum>x=a..b. e'   is the same as  'setsum (%x. e) {a..b}'
-  '\<Sum>x=a..<b. e'  is the same as  'setsum (%x. e) {a..<b}'
-  '\<Sum>x<k. e'      is the same as  'setsum (%x. e) {..<k}'
-
-  Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e'
-  now translates into 'setsum' as above.
-
-* HOL: Finite set induction: In Isar proofs, the insert case is now
-  "case (insert x F)" instead of the old counterintuitive "case (insert F x)".
-
-* HOL/Simplifier:
-
-  - Is now set up to reason about transitivity chains involving "trancl"
-  (r^+) and "rtrancl" (r^*) by setting up tactics provided by
-  Provers/trancl.ML as additional solvers.  INCOMPATIBILITY: old proofs break
-  occasionally as simplification may now solve more goals than previously.
-
-  - Converts x <= y into x = y if assumption y <= x is present.  Works for
-  all partial orders (class "order"), in particular numbers and sets. For
-  linear orders (e.g. numbers) it treats ~ x < y just like y <= x.
-
-  - Simproc for "let x = a in f x"
-  If a is a free or bound variable or a constant then the let is unfolded.
-  Otherwise first a is simplified to a', and then f a' is simplified to
-  g. If possible we abstract a' from g arriving at "let x = a' in g' x",
-  otherwise we unfold the let and arrive at g. The simproc can be 
-  enabled/disabled by the reference use_let_simproc. Potential
-  INCOMPATIBILITY since simplification is more powerful by default.
- 
-* HOL: new 'isatool dimacs2hol' to convert files in DIMACS CNF format
-  (containing Boolean satisfiability problems) into Isabelle/HOL theories.
-
-
-*** HOLCF ***
-
-* HOLCF: discontinued special version of 'constdefs' (which used to
-  support continuous functions) in favor of the general Pure one with
-  full type-inference.
-
-
-*** ZF ***
-
-* ZF/ex/{Group,Ring}: examples in abstract algebra, including the
-  First Isomorphism Theorem (on quotienting by the kernel of a
-  homomorphism).
-
-* ZF/Simplifier: install second copy of type solver that actually
-  makes use of TC rules declared to Isar proof contexts (or locales);
-  the old version is still required for ML proof scripts.
+* Provers: Simplifier and Classical Reasoner now support proof context
+  dependent plug-ins (simprocs, solvers, wrappers etc.).  These extra
+  components are stored in the theory and patched into the
+  simpset/claset when used in an Isar proof context.  Context
+  dependent components are maintained by the following theory
+  operations:
+
+    Simplifier.add_context_simprocs
+    Simplifier.del_context_simprocs
+    Simplifier.set_context_subgoaler
+    Simplifier.reset_context_subgoaler
+    Simplifier.add_context_looper
+    Simplifier.del_context_looper
+    Simplifier.add_context_unsafe_solver
+    Simplifier.add_context_safe_solver
+
+    Classical.add_context_safe_wrapper
+    Classical.del_context_safe_wrapper
+    Classical.add_context_unsafe_wrapper
+    Classical.del_context_unsafe_wrapper
+
+  IMPORTANT NOTE: proof tools (methods etc.) need to use
+  local_simpset_of and local_claset_of to instead of the primitive
+  Simplifier.get_local_simpset and Classical.get_local_claset,
+  respectively, in order to see the context dependent fields!
 
 
 
 New in Isabelle2004 (April 2004)
 --------------------------------