diff -r e6d738f2b9a9 -r b59781f2b809 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Nov 27 16:48:19 1996 +0100
+++ b/src/HOL/HOL.thy	Wed Nov 27 16:51:15 1996 +0100
@@ -3,23 +3,17 @@
     Author:     Tobias Nipkow
     Copyright   1993  University of Cambridge
 
-Higher-Order Logic
+Higher-Order Logic.
 *)
 
 HOL = CPure +
 
+
+(** Core syntax **)
+
 classes
   term < logic
 
-axclass
-  plus < term
-
-axclass
-  minus < term
-
-axclass
-  times < term
-
 default
   term
 
@@ -57,13 +51,27 @@
   "|"           :: [bool, bool] => bool             (infixr 30)
   "-->"         :: [bool, bool] => bool             (infixr 25)
 
-  (* Overloaded Constants *)
+
+(* Overloaded Constants *)
+
+axclass
+  plus < term
 
+axclass
+  minus < term
+
+axclass
+  times < term
+
+consts
   "+"           :: ['a::plus, 'a] => 'a             (infixl 65)
   "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
   "*"           :: ['a::times, 'a] => 'a            (infixl 70)
 
 
+
+(** Additional concrete syntax **)
+
 types
   letbinds  letbind
   case_syn  cases_syn
@@ -72,7 +80,7 @@
 
   "~="          :: ['a, 'a] => bool                 (infixl 50)
 
-  "@Eps"        :: [pttrn,bool] => 'a               ("(3@ _./ _)" 10)
+  "@Eps"        :: [pttrn, bool] => 'a              ("(3@ _./ _)" 10)
 
   (* Alternative Quantifiers *)
 
@@ -96,13 +104,34 @@
 
 translations
   "x ~= y"      == "~ (x = y)"
-  "@ x.b"       == "Eps(%x.b)"
+  "@ x.b"       == "Eps (%x. b)"
   "ALL xs. P"   => "! xs. P"
   "EX xs. P"    => "? xs. P"
   "EX! xs. P"   => "?! xs. P"
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   "let x = a in e"        == "Let a (%x. e)"
 
+
+syntax (symbols)
+  not           :: bool => bool                     ("\\<not> _" [40] 40)
+  "op &"        :: [bool, bool] => bool             (infixr "\\<and>" 35)
+  "op |"        :: [bool, bool] => bool             (infixr "\\<or>" 30)
+  "op -->"      :: [bool, bool] => bool             (infixr "\\<midarrow>\\<rightarrow>" 25)
+  "op o"        :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl "\\<circ>" 55)
+  "op ~="       :: ['a, 'a] => bool                 (infixl "\\<noteq>" 50)
+  "@Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" 10)
+  "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" 10)
+  "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" 10)
+  "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" 10)
+  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" 10)
+  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" 10)
+  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" 10)
+  "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<mapsto>/ _)" 10)
+
+
+
+(** Rules and definitions **)
+
 rules
 
   eq_reflection "(x=y) ==> (x==y)"
@@ -147,6 +176,7 @@
 
 end
 
+
 ML
 
 (** Choice between the HOL and Isabelle style of quantifiers **)
@@ -168,6 +198,3 @@
 
 (* start 8bit 2 *)
 (* end 8bit 2 *)
-
-
-