--- a/NEWS Thu Apr 21 22:00:28 2005 +0200
+++ b/NEWS Thu Apr 21 22:02:06 2005 +0200
@@ -189,6 +189,13 @@
* Isar: new syntax 'name(i-j, i-, i, ...)' for referring to specific
selections of theorems in named facts via indices.
+* Pure: reorganized bootstrapping of the Pure theories; CPure is now
+ derived from Pure, which contains all common declarations already.
+ Both theories are defined via plain Isabelle/Isar .thy files.
+ INCOMPATIBILITY: elements of CPure (such as the CPure.intro /
+ CPure.elim / CPure.dest attributes) now appear in the Pure name
+ space; use isatool fixcpure to adapt your theory and ML sources.
+
*** Document preparation ***