NEWS
changeset 15801 d2f5ca3c048d
parent 15778 98af3693f6b3
child 15852 4f1a78454452
     1.1 --- a/NEWS	Thu Apr 21 22:00:28 2005 +0200
     1.2 +++ b/NEWS	Thu Apr 21 22:02:06 2005 +0200
     1.3 @@ -189,6 +189,13 @@
     1.4  * Isar: new syntax 'name(i-j, i-, i, ...)' for referring to specific
     1.5    selections of theorems in named facts via indices.
     1.6  
     1.7 +* Pure: reorganized bootstrapping of the Pure theories; CPure is now
     1.8 +  derived from Pure, which contains all common declarations already.
     1.9 +  Both theories are defined via plain Isabelle/Isar .thy files.
    1.10 +  INCOMPATIBILITY: elements of CPure (such as the CPure.intro /
    1.11 +  CPure.elim / CPure.dest attributes) now appear in the Pure name
    1.12 +  space; use isatool fixcpure to adapt your theory and ML sources.
    1.13 +
    1.14  
    1.15  *** Document preparation ***
    1.16