src/HOL/HOL.thy
changeset 3842 b55686a7b22c
parent 3820 46b255e140dc
child 3947 eb707467f8c5
     1.1 --- a/src/HOL/HOL.thy	Fri Oct 10 18:37:49 1997 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Oct 10 19:02:28 1997 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4  
     1.5  translations
     1.6    "x ~= y"      == "~ (x = y)"
     1.7 -  "@ x.b"       == "Eps (%x. b)"
     1.8 +  "@ x. b"      == "Eps (%x. b)"
     1.9    "ALL xs. P"   => "! xs. P"
    1.10    "EX xs. P"    => "? xs. P"
    1.11    "EX! xs. P"   => "?! xs. P"
    1.12 @@ -149,18 +149,18 @@
    1.13  
    1.14    refl          "t = (t::'a)"
    1.15    subst         "[| s = t; P(s) |] ==> P(t::'a)"
    1.16 -  ext           "(!!x::'a. (f(x)::'b) = g(x)) ==> (%x.f(x)) = (%x.g(x))"
    1.17 -  selectI       "P(x::'a) ==> P(@x.P(x))"
    1.18 +  ext           "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
    1.19 +  selectI       "P (x::'a) ==> P (@x. P x)"
    1.20  
    1.21    impI          "(P ==> Q) ==> P-->Q"
    1.22    mp            "[| P-->Q;  P |] ==> Q"
    1.23  
    1.24  defs
    1.25  
    1.26 -  True_def      "True      == ((%x::bool.x)=(%x.x))"
    1.27 -  All_def       "All(P)    == (P = (%x.True))"
    1.28 -  Ex_def        "Ex(P)     == P(@x.P(x))"
    1.29 -  False_def     "False     == (!P.P)"
    1.30 +  True_def      "True      == ((%x::bool. x) = (%x. x))"
    1.31 +  All_def       "All(P)    == (P = (%x. True))"
    1.32 +  Ex_def        "Ex(P)     == P(@x. P(x))"
    1.33 +  False_def     "False     == (!P. P)"
    1.34    not_def       "~ P       == P-->False"
    1.35    and_def       "P & Q     == !R. (P-->Q-->R) --> R"
    1.36    or_def        "P | Q     == !R. (P-->R) --> (Q-->R) --> R"