author | wenzelm |

Tue Jul 15 11:02:43 2008 +0200 (2008-07-15) | |

changeset 27599 | ca23ef50c178 |

parent 27598 | b66e257b75f5 |

child 27600 | 90cbc874549f |

added command 'linear_undo';

tuned;

tuned;

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