diff -r 2859c94d67d4 -r b5a642c4d085 NEWS
--- a/NEWS	Wed Nov 29 15:45:02 2006 +0100
+++ b/NEWS	Wed Nov 29 15:47:05 2006 +0100
@@ -254,15 +254,14 @@
 isar-ref manual.  Examples:
 
   axiomatization
-    eq  (infix "===" 50)
-    where eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
-
-  definition
-    "f x y = x + y + 1"
-    "g x = f x x"
+    eq  (infix "===" 50) where
+    eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
+
+  definition "f x y = x + y + 1"
+  definition g where "g x = f x x"
 
   abbreviation
-    neq  (infix "=!=" 50)
+    neq  (infix "=!=" 50) where
     "x =!= y == ~ (x === y)"
 
 These specifications may be also used in a locale context.  Then the