diff -r 6254f50e5ec9 -r a9f7ff3a464c HOL.thy
--- a/HOL.thy	Fri Sep 16 15:48:20 1994 +0200
+++ b/HOL.thy	Wed Sep 21 15:40:41 1994 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/hol.thy
+(*  Title:      HOL/HOL.thy
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1993  University of Cambridge
@@ -10,8 +10,14 @@
 
 classes
   term < logic
+
+axclass
   plus < term
+
+axclass
   minus < term
+
+axclass
   times < term
 
 default
@@ -19,8 +25,6 @@
 
 types
   bool
-  letbinds  letbind
-  case_syn  cases_syn
 
 arities
   fun :: (term, term) term
@@ -43,31 +47,13 @@
   All           :: "('a => bool) => bool"             (binder "! " 10)
   Ex            :: "('a => bool) => bool"             (binder "? " 10)
   Ex1           :: "('a => bool) => bool"             (binder "?! " 10)
-
   Let           :: "['a, 'a => 'b] => 'b"
-  "_bind"       :: "[idt, 'a] => letbind"             ("(2_ =/ _)" 10)
-  ""            :: "letbind => letbinds"              ("_")
-  "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
-  "_Let"        :: "[letbinds, 'a] => 'a"            ("(let (_)/ in (_))" 10)
-
-  (* Case expressions *)
-
-  "@case"            :: "['a, cases_syn] => 'b"		("(case _ of/ _)" 10)
-  "@case1"           :: "['a, 'b] => case_syn"		("(2_ =>/ _)" 10)
-  ""                 :: "case_syn => cases_syn"		("_")
-  "@case2"           :: "[case_syn,cases_syn] => cases_syn"	("_/ | _")
-
-  (* Alternative Quantifiers *)
-
-  "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)
-  "*Ex"         :: "[idts, bool] => bool"             ("(3EX _./ _)" 10)
-  "*Ex1"        :: "[idts, bool] => bool"             ("(3EX! _./ _)" 10)
 
   (* Infixes *)
 
   o             :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixr 50)
   "="           :: "['a, 'a] => bool"                 (infixl 50)
-  "~="          :: "['a, 'a] => bool"                 ("(_ ~=/ _)" [50, 51] 50)
+(*"~="          :: "['a, 'a] => bool"                 (infixl 50)*)
   "&"           :: "[bool, bool] => bool"             (infixr 35)
   "|"           :: "[bool, bool] => bool"             (infixr 30)
   "-->"         :: "[bool, bool] => bool"             (infixr 25)
@@ -79,13 +65,42 @@
   "*"           :: "['a::times, 'a] => 'a"            (infixl 70)
 
 
+types
+  letbinds  letbind
+  case_syn  cases_syn
+
+syntax
+
+  "~="          :: "['a, 'a] => bool"                 (infixl 50)
+
+  (* Alternative Quantifiers *)
+
+  "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)
+  "*Ex"         :: "[idts, bool] => bool"             ("(3EX _./ _)" 10)
+  "*Ex1"        :: "[idts, bool] => bool"             ("(3EX! _./ _)" 10)
+
+  (* Let expressions *)
+
+  "_bind"       :: "[idt, 'a] => letbind"             ("(2_ =/ _)" 10)
+  ""            :: "letbind => letbinds"              ("_")
+  "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
+  "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
+
+  (* Case expressions *)
+
+  "@case"       :: "['a, cases_syn] => 'b"            ("(case _ of/ _)" 10)
+  "@case1"      :: "['a, 'b] => case_syn"             ("(2_ =>/ _)" 10)
+  ""            :: "case_syn => cases_syn"            ("_")
+  "@case2"      :: "[case_syn, cases_syn] => cases_syn"   ("_/ | _")
+
 translations
+  "x ~= y"      == "~ (x = y)"
   "ALL xs. P"   => "! xs. P"
   "EX xs. P"    => "? xs. P"
   "EX! xs. P"   => "?! xs. P"
-  "x ~= y"      == "~ (x = y)"
-  "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
-  "let x = a in e" == "Let(a, %x. e)"
+  "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
+  "let x = a in e"          == "Let(a, %x. e)"
+
 
 rules
 
@@ -103,15 +118,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       "~ 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)"
+  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 *)