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