diff -r 281295a1bbaa -r c73d62ce9d1c src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Wed Oct 15 11:02:28 2003 +0200
+++ b/src/FOL/IFOL.thy	Thu Oct 16 10:31:40 2003 +0200
@@ -64,6 +64,13 @@
 
 local
 
+finalconsts
+  False All Ex
+  "op ="
+  "op &"
+  "op |"
+  "op -->"
+
 axioms
 
   (* Equality *)
@@ -86,18 +93,6 @@
 
   FalseE:       "False ==> P"
 
-
-  (* Definitions *)
-
-  True_def:     "True  == False-->False"
-  not_def:      "~P    == P-->False"
-  iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
-
-  (* Unique existence *)
-
-  ex1_def:      "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
-
-
   (* Quantifiers *)
 
   allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
@@ -112,6 +107,17 @@
   iff_reflection: "(P<->Q) ==> (P==Q)"
 
 
+defs
+  (* Definitions *)
+
+  True_def:     "True  == False-->False"
+  not_def:      "~P    == P-->False"
+  iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
+
+  (* Unique existence *)
+
+  ex1_def:      "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+
 
 subsection {* Lemmas and proof tools *}