HOL.thy

--- a/HOL.thy	Fri Jun 24 15:11:39 1994 +0200
+++ b/HOL.thy	Wed Jun 29 12:04:04 1994 +0200
@@ -93,9 +93,9 @@
 
   (* Basic Rules *)
 
-  refl          "t = t::'a"
+  refl          "t = (t::'a)"
   subst         "[| s = t; P(s) |] ==> P(t::'a)"
-  ext           "(!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x))"
+  ext           "(!!x::'a. (f(x)::'b) = g(x)) ==> (%x.f(x)) = (%x.g(x))"
   selectI       "P(x::'a) ==> P(@x.P(x))"
 
   impI          "(P ==> Q) ==> P-->Q"