diff -r 9459592608e2 -r 9e9feb5f15dc HOL.thy
--- a/HOL.thy	Sun Apr 24 11:27:38 1994 +0200
+++ b/HOL.thy	Tue May 03 11:30:09 1994 +0200
@@ -19,8 +19,8 @@
 
 types
   bool
-  letbinds, letbind 0
-  case_syn,cases_syn 0
+  letbinds  letbind
+  case_syn  cases_syn
 
 arities
   fun :: (term, term) term
@@ -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       "~ P      == P-->False"
+  and_def       "P & Q    == !R. (P-->Q-->R) --> R"
+  or_def        "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,9 @@
 
   (* 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)))"
-
-  if_def        "if == (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
+  Inv_def       "Inv(f::'a=>'b)  == (% y. @x. f(x)=y)"
+  o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
+  if_def        "if(P,x,y) == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
 
 end