changeset 90 | 5c7a69cef18b |
parent 71 | 9e9feb5f15dc |
child 145 | a9f7ff3a464c |
--- 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"