added command 'linear_undo';
authorwenzelm
Tue Jul 15 11:02:43 2008 +0200 (2008-07-15)
changeset 27599ca23ef50c178
parent 27598 b66e257b75f5
child 27600 90cbc874549f
added command 'linear_undo';
tuned;
NEWS
     1.1 --- a/NEWS	Tue Jul 15 10:59:14 2008 +0200
     1.2 +++ b/NEWS	Tue Jul 15 11:02:43 2008 +0200
     1.3 @@ -4,12 +4,21 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 -*** Pure ***
     1.8 +*** General ***
     1.9 +
    1.10 +* Generalized Isar history, with support for linear undo, direct state
    1.11 +addressing etc.
    1.12  
    1.13  * Recovered hiding of consts, which was accidentally broken in
    1.14  Isabelle2007.  Potential INCOMPATIBILITY, ``hide const c'' really
    1.15  makes c inaccessible; consider using ``hide (open) const c'' instead.
    1.16  
    1.17 +* Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
    1.18 +interface instead.
    1.19 +
    1.20 +
    1.21 +*** Pure ***
    1.22 +
    1.23  * Command 'instance': attached definitions now longer accepted.
    1.24  INCOMPATIBILITY, use proper 'instantiation' target.
    1.25  
    1.26 @@ -28,9 +37,6 @@
    1.27  serializations are set.  Refer to the corresponding ML counterpart
    1.28  directly in that cases.
    1.29  
    1.30 -* Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
    1.31 -interface instead.
    1.32 -
    1.33  
    1.34  *** Document preparation ***
    1.35  
    1.36 @@ -41,10 +47,11 @@
    1.37  
    1.38  *** HOL ***
    1.39  
    1.40 -* HOL/Library/GCD:  Curried operations gcd, lcm (for nat) and zgcd, zlcm (for int);
    1.41 -carried together from various gcd/lcm developements in the HOL Distribution.
    1.42 -zgcd and zlcm replace former igcd and ilcm;  corresponding theorems renamed
    1.43 -accordingly.  INCOMPATIBILY.  To recover tupled syntax, use syntax declarations like:
    1.44 +* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
    1.45 +zlcm (for int); carried together from various gcd/lcm developements in
    1.46 +the HOL Distribution.  zgcd and zlcm replace former igcd and ilcm;
    1.47 +corresponding theorems renamed accordingly.  INCOMPATIBILY.  To
    1.48 +recover tupled syntax, use syntax declarations like:
    1.49  
    1.50      hide (open) const gcd
    1.51      abbreviation gcd where
    1.52 @@ -59,11 +66,12 @@
    1.53  * Integrated image HOL-Complex with HOL.  Entry points Main.thy and
    1.54  Complex_Main.thy remain as they are.
    1.55  
    1.56 -* New image HOL-Plain provides a minimal HOL with the most important tools
    1.57 -available (inductive, datatype, primrec, ...).  By convention the corresponding
    1.58 -theory Plain should be ancestor of every further (library) theory.  Some library
    1.59 -theories now have ancestor Plain (instead of Main), thus theory Main
    1.60 -occasionally has to be imported explicitly.
    1.61 +* New image HOL-Plain provides a minimal HOL with the most important
    1.62 +tools available (inductive, datatype, primrec, ...).  By convention
    1.63 +the corresponding theory Plain should be ancestor of every further
    1.64 +(library) theory.  Some library theories now have ancestor Plain
    1.65 +(instead of Main), thus theory Main occasionally has to be imported
    1.66 +explicitly.
    1.67  
    1.68  * Methods "case_tac" and "induct_tac" now refer to the very same rules
    1.69  as the structured Isar versions "cases" and "induct", cf. the