# HG changeset patch
# User wenzelm
# Date 959004223 -7200
# Node ID 7c04c98132c4f4082b0b350b2fe4388952b99cba
# Parent  af5e09b6c20834dd91e00dfc778d6cf72a5b696d
* Pure: changed syntax of local blocks from {{ }} to { };
* Pure: syntax of sorts made inner, i.e. have to write "{a, b, c}";

diff -r af5e09b6c208 -r 7c04c98132c4 NEWS
--- 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;