diff -r a910a65478be -r d199410f1db1 Set.thy
--- a/Set.thy	Tue Sep 28 14:27:31 1993 +0100
+++ b/Set.thy	Mon Oct 04 15:43:54 1993 +0100
@@ -19,43 +19,43 @@
 
   (* Constants *)
 
-  Collect       :: "('a => bool) => 'a set"                 (*comprehension*)
-  Compl         :: "('a set) => 'a set"                     (*complement*)
-  Int           :: "['a set, 'a set] => 'a set"         (infixl 70)
-  Un            :: "['a set, 'a set] => 'a set"         (infixl 65)
-  UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"       (*general*)
-  UNION1        :: "['a => 'b set] => 'b set"           (binder "UN " 10)
-  INTER1        :: "['a => 'b set] => 'b set"           (binder "INT " 10)
-  Union, Inter  :: "(('a set)set) => 'a set"                (*of a set*)
-  range         :: "('a => 'b) => 'b set"                   (*of function*)
-  Ball, Bex     :: "['a set, 'a => bool] => bool"           (*bounded quantifiers*)
-  inj, surj     :: "('a => 'b) => bool"                     (*injective/surjective*)
+  Collect       :: "('a => bool) => 'a set"               (*comprehension*)
+  Compl         :: "('a set) => 'a set"                   (*complement*)
+  Int           :: "['a set, 'a set] => 'a set"       (infixl 70)
+  Un            :: "['a set, 'a set] => 'a set"       (infixl 65)
+  UNION, INTER  :: "['a set, 'a => 'b set] => 'b set"     (*general*)
+  UNION1        :: "['a => 'b set] => 'b set"         (binder "UN " 10)
+  INTER1        :: "['a => 'b set] => 'b set"         (binder "INT " 10)
+  Union, Inter  :: "(('a set)set) => 'a set"              (*of a set*)
+  range         :: "('a => 'b) => 'b set"                 (*of function*)
+  Ball, Bex     :: "['a set, 'a => bool] => bool"         (*bounded quantifiers*)
+  inj, surj     :: "('a => 'b) => bool"                   (*injective/surjective*)
   inj_onto      :: "['a => 'b, 'a set] => bool"
-  "``"          :: "['a => 'b, 'a set] => ('b set)"     (infixl 90)
-  ":"           :: "['a, 'a set] => bool" (infixl 50)       (*membership*)
+  "``"          :: "['a => 'b, 'a set] => ('b set)"   (infixl 90)
+  ":"           :: "['a, 'a set] => bool"             (infixl 50) (*membership*)
 
   (* Finite Sets *)
 
   insert        :: "['a, 'a set] => 'a set"
-  "{}"          :: "'a set"                             ("{}")
-  "@Finset"     :: "args => 'a set"                     ("{(_)}")
+  "{}"          :: "'a set"                           ("{}")
+  "@Finset"     :: "args => 'a set"                   ("{(_)}")
 
 
   (** Binding Constants **)
 
-  "@Coll"       :: "[idt, bool] => 'a set"              ("(1{_./ _})")  (*collection*)
+  "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})")  (*collection*)
 
   (* Big Intersection / Union *)
 
-  "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"    ("(3INT _:_./ _)" 10)
-  "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"    ("(3UN _:_./ _)" 10)
+  "@INTER"      :: "[idt, 'a set, 'b set] => 'b set"  ("(3INT _:_./ _)" 10)
+  "@UNION"      :: "[idt, 'a set, 'b set] => 'b set"  ("(3UN _:_./ _)" 10)
 
   (* Bounded Quantifiers *)
 
-  "@Ball"       :: "[idt, 'a set, bool] => bool"        ("(3! _:_./ _)" 10)
-  "@Bex"        :: "[idt, 'a set, bool] => bool"        ("(3? _:_./ _)" 10)
-  "*Ball"       :: "[idt, 'a set, bool] => bool"        ("(3ALL _:_./ _)" 10)
-  "*Bex"        :: "[idt, 'a set, bool] => bool"        ("(3EX _:_./ _)" 10)
+  "@Ball"       :: "[idt, 'a set, bool] => bool"      ("(3! _:_./ _)" 10)
+  "@Bex"        :: "[idt, 'a set, bool] => bool"      ("(3? _:_./ _)" 10)
+  "*Ball"       :: "[idt, 'a set, bool] => bool"      ("(3ALL _:_./ _)" 10)
+  "*Bex"        :: "[idt, 'a set, bool] => bool"      ("(3EX _:_./ _)" 10)
 
 
 translations
@@ -107,5 +107,5 @@
 ML
 
 val print_ast_translation =
-  map HOL.mk_alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
+  map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];