replaced some "rules" by "defs"

--- a/HOL.thy	Tue Oct 04 13:00:20 1994 +0100
+++ b/HOL.thy	Thu Oct 06 09:36:40 1994 +0100
@@ -116,7 +116,7 @@
   impI          "(P ==> Q) ==> P-->Q"
   mp            "[| P-->Q;  P |] ==> Q"
 
-  (* Definitions *)
+defs
 
   True_def      "True      == ((%x::bool.x)=(%x.x))"
   All_def       "All(P)    == (P = (%x.True))"
@@ -126,15 +126,17 @@
   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)"
 
+rules
   (* Axioms *)
 
   iff           "(P-->Q) --> (Q-->P) --> (P=Q)"
   True_or_False "(P=True) | (P=False)"
 
+defs
   (* Misc Definitions *)
 
+  Let_def       "Let(s, f) == f(s)"
   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)"