--- a/HOL.thy Sun Apr 24 11:27:38 1994 +0200
+++ b/HOL.thy Tue May 03 11:30:09 1994 +0200
@@ -19,8 +19,8 @@
types
bool
- letbinds, letbind 0
- case_syn,cases_syn 0
+ letbinds letbind
+ case_syn cases_syn
arities
fun :: (term, term) term
@@ -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 "~ P == P-->False"
+ 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)"
(* Axioms *)
@@ -120,10 +120,9 @@
(* 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)))"
-
- if_def "if == (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
+ 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)"
end