# HG changeset patch
# User wenzelm
# Date 1216112563 -7200
# Node ID ca23ef50c1783426d174f10a23b35e8fd3acc051
# Parent  b66e257b75f53e3c6c941ebb93d9ffdb91cb1354
added command 'linear_undo';
tuned;

diff -r b66e257b75f5 -r ca23ef50c178 NEWS
--- a/NEWS	Tue Jul 15 10:59:14 2008 +0200
+++ b/NEWS	Tue Jul 15 11:02:43 2008 +0200
@@ -4,12 +4,21 @@
 New in this Isabelle version
 ----------------------------
 
-*** Pure ***
+*** General ***
+
+* Generalized Isar history, with support for linear undo, direct state
+addressing etc.
 
 * Recovered hiding of consts, which was accidentally broken in
 Isabelle2007.  Potential INCOMPATIBILITY, ``hide const c'' really
 makes c inaccessible; consider using ``hide (open) const c'' instead.
 
+* Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
+interface instead.
+
+
+*** Pure ***
+
 * Command 'instance': attached definitions now longer accepted.
 INCOMPATIBILITY, use proper 'instantiation' target.
 
@@ -28,9 +37,6 @@
 serializations are set.  Refer to the corresponding ML counterpart
 directly in that cases.
 
-* Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
-interface instead.
-
 
 *** Document preparation ***
 
@@ -41,10 +47,11 @@
 
 *** HOL ***
 
-* HOL/Library/GCD:  Curried operations gcd, lcm (for nat) and zgcd, zlcm (for int);
-carried together from various gcd/lcm developements in the HOL Distribution.
-zgcd and zlcm replace former igcd and ilcm;  corresponding theorems renamed
-accordingly.  INCOMPATIBILY.  To recover tupled syntax, use syntax declarations like:
+* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
+zlcm (for int); carried together from various gcd/lcm developements in
+the HOL Distribution.  zgcd and zlcm replace former igcd and ilcm;
+corresponding theorems renamed accordingly.  INCOMPATIBILY.  To
+recover tupled syntax, use syntax declarations like:
 
     hide (open) const gcd
     abbreviation gcd where
@@ -59,11 +66,12 @@
 * Integrated image HOL-Complex with HOL.  Entry points Main.thy and
 Complex_Main.thy remain as they are.
 
-* New image HOL-Plain provides a minimal HOL with the most important tools
-available (inductive, datatype, primrec, ...).  By convention the corresponding
-theory Plain should be ancestor of every further (library) theory.  Some library
-theories now have ancestor Plain (instead of Main), thus theory Main
-occasionally has to be imported explicitly.
+* New image HOL-Plain provides a minimal HOL with the most important
+tools available (inductive, datatype, primrec, ...).  By convention
+the corresponding theory Plain should be ancestor of every further
+(library) theory.  Some library theories now have ancestor Plain
+(instead of Main), thus theory Main occasionally has to be imported
+explicitly.
 
 * Methods "case_tac" and "induct_tac" now refer to the very same rules
 as the structured Isar versions "cases" and "induct", cf. the