diff -r 52771c21d9ca -r 14b9286ed036 HOL.thy
--- a/HOL.thy	Wed Apr 06 16:31:06 1994 +0200
+++ b/HOL.thy	Tue Apr 19 10:50:00 1994 +0200
@@ -103,15 +103,15 @@
 
   (* Definitions *)
 
-  True_def      "True = ((%x::bool.x)=(%x.x))"
-  All_def       "All  = (%P. P = (%x.True))"
-  Ex_def        "Ex   = (%P. P(@x.P(x)))"
-  False_def     "False = (!P.P)"
-  not_def       "not  = (%P. P-->False)"
-  and_def       "op & = (%P Q. !R. (P-->Q-->R) --> R)"
-  or_def        "op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
-  Ex1_def       "Ex1  = (%P. ? x. P(x) & (! y. P(y) --> y=x))"
-  Let_def       "Let(s, f) = f(s)"
+  True_def      "True == ((%x::bool.x)=(%x.x))"
+  All_def       "All  == (%P. P = (%x.True))"
+  Ex_def        "Ex   == (%P. P(@x.P(x)))"
+  False_def     "False == (!P.P)"
+  not_def       "not  == (%P. P-->False)"
+  and_def       "op & == (%P Q. !R. (P-->Q-->R) --> R)"
+  or_def        "op | == (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
+  Ex1_def       "Ex1  == (%P. ? x. P(x) & (! y. P(y) --> y=x))"
+  Let_def       "Let(s, f) == f(s)"
 
   (* Axioms *)
 
@@ -120,10 +120,10 @@
 
   (* Misc Definitions *)
 
-  Inv_def       "Inv = (%(f::'a=>'b) y. @x. f(x)=y)"
-  o_def         "op o = (%(f::'b=>'c) g (x::'a). f(g(x)))"
+  Inv_def       "Inv == (%(f::'a=>'b) y. @x. f(x)=y)"
+  o_def         "op o == (%(f::'b=>'c) g (x::'a). f(g(x)))"
 
-  if_def        "if = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
+  if_def        "if == (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
 
 end