--- a/HOL.thy Wed Apr 06 16:31:06 1994 +0200
+++ b/HOL.thy Tue Apr 19 10:50:00 1994 +0200
@@ -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 "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)"
(* Axioms *)
@@ -120,10 +120,10 @@
(* 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)))"
+ 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))"
+ if_def "if == (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
end