--- 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;