# HG changeset patch
# User wenzelm
# Date 1212010416 -7200
# Node ID 9e39f5403db77b2643fe32db3a6fa6691ccf26b2
# Parent  c1960cad50176de2ad7bf979d8cf8ae30fb51a5f
misc tuning for Isabelle2008;

diff -r c1960cad5017 -r 9e39f5403db7 NEWS
--- a/NEWS	Wed May 28 23:33:15 2008 +0200
+++ b/NEWS	Wed May 28 23:33:36 2008 +0200
@@ -1,8 +1,8 @@
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
-New in this Isabelle version
-----------------------------
+New in Isabelle2008 (June 2008)
+-------------------------------
 
 *** General ***
 
@@ -121,13 +121,9 @@
 value unchanged, can be redefined via \definecolor); no longer sets
 "a4paper" option (unnecessary or even intrusive).
 
-* Antiquotation "lemma" takes a proposition and a simple method text
-as argument and asserts that the proposition is provable by the
-corresponding method invocation.  Prints text of proposition, as does
-antiquotation "prop".  A simple method text is either a method name or
-a method name plus (optional) method arguments in parentheses,
-mimicking the conventions known from Isar proof text.  Useful for
-illustration of presented theorems by particular examples.
+* Antiquotation @{lemma A method} proves proposition A by the given
+method (either a method name or a method name plus (optional) method
+arguments in parentheses) and prints A just like @{prop A}.
 
 
 *** HOL ***
@@ -136,12 +132,12 @@
 
   INCOMPATIBILITIES:
 
-  - Definitions of overloaded constants on sets have to be
-    replaced by definitions on => and bool.
+  - Definitions of overloaded constants on sets have to be replaced by
+    definitions on => and bool.
 
   - Some definitions of overloaded operators on sets can now be proved
-    using the definitions of the operators on => and bool.
-    Therefore, the following theorems have been renamed:
+    using the definitions of the operators on => and bool.  Therefore,
+    the following theorems have been renamed:
 
       subset_def   -> subset_eq
       psubset_def  -> psubset_eq
@@ -162,8 +158,8 @@
       have "P (S::'a set)" <...>
       then have "EX S. P S" ..
 
-    no longer works (due to the incompleteness of the HO unification algorithm)
-    and must be replaced by the pattern
+    no longer works (due to the incompleteness of the HO unification
+    algorithm) and must be replaced by the pattern
 
       have "EX S. P S"
       proof
@@ -177,8 +173,8 @@
       also have "S = T" <...>
       finally have "P T" .
 
-    no longer works (for similar reasons as the previous example) and must be
-    replaced by something like
+    no longer works (for similar reasons as the previous example) and
+    must be replaced by something like
 
       have "P (S::'a set)" <...>
       moreover have "S = T" <...>
@@ -189,8 +185,9 @@
 
       Type ("set", [T]) => ...
 
-    must be rewritten. Moreover, functions like strip_type or binder_types no
-    longer return the right value when applied to a type of the form
+    must be rewritten. Moreover, functions like strip_type or
+    binder_types no longer return the right value when applied to a
+    type of the form
 
       T1 => ... => Tn => U => bool
 
@@ -234,8 +231,8 @@
 
 * Library/Option_ord.thy: Canonical order on option type.
 
-* Library/RBT.thy: New theory of red-black trees, an efficient
-implementation of finite maps.
+* Library/RBT.thy: Red-black trees, an efficient implementation of
+finite maps.
 
 * Library/Countable.thy: Type class for countable types.
 
@@ -327,10 +324,10 @@
 reconstruction_modulus, reconstruction_sorts renamed
 sledgehammer_modulus, sledgehammer_sorts.  INCOMPATIBILITY.
 
-* More flexible generation of measure functions for termination proofs:
-Measure functions can be declared by proving a rule of the form
-"is_measure f" and giving it the [measure_function] attribute. The
-"is_measure" predicate is logically meaningless (always true), and
+* More flexible generation of measure functions for termination
+proofs: Measure functions can be declared by proving a rule of the
+form "is_measure f" and giving it the [measure_function] attribute.
+The "is_measure" predicate is logically meaningless (always true), and
 just guides the heuristic.  To find suitable measure functions, the
 termination prover sets up the goal "is_measure ?f" of the appropriate
 type and generates all solutions by prolog-style backwards proof using
@@ -379,7 +376,7 @@
 print_mode_active, PrintMode.setmp etc.  INCOMPATIBILITY.
 
 * Functions system/system_out provide a robust way to invoke external
-shell commands, with propagation of interrupts (after Poly/ML 5.2).
+shell commands, with propagation of interrupts (requires Poly/ML 5.2).
 Do not use OS.Process.system etc. from the basis library!