* Pure: changed syntax of local blocks from {{ }} to { };
* Pure: syntax of sorts made inner, i.e. have to write "{a, b, c}";

--- a/NEWS	Mon May 22 13:29:21 2000 +0200
+++ b/NEWS	Mon May 22 16:03:43 2000 +0200
@@ -35,6 +35,8 @@
 Lfp, Gfp, WF); this only affects ML packages that refer to const names
 internally;
 
+* Isar: changed syntax of local blocks from {{ }} to { };
+
 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
 
 * LaTeX: several improvements of isabelle.sty;
@@ -72,6 +74,11 @@
 certain proof methods; internally, case names are attached to theorems
 as "tags";
 
+* Pure: changed syntax of local blocks from {{ }} to { };
+
+* Pure: syntax of sorts made inner, i.e. have to write "{a, b, c}"
+instead of {a, b, c};
+
 * Pure now provides its own version of intro/elim/dest attributes;
 useful for building new logics, but beware of confusion with the
 Provers/classical ones;