diff -r 6254f50e5ec9 -r a9f7ff3a464c Set.thy
--- a/Set.thy	Fri Sep 16 15:48:20 1994 +0200
+++ b/Set.thy	Wed Sep 21 15:40:41 1994 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/set.thy
+(*  Title:      HOL/Set.thy
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1993  University of Cambridge
@@ -11,14 +11,13 @@
 
 arities
   set :: (term) term
-  set :: (term) ord
-  set :: (term) minus
 
+instance
+  set :: (term) {ord, minus}
 
 consts
-
-  (* Constants *)
-
+  "{}"          :: "'a set"                           ("{}")
+  insert        :: "['a, 'a set] => 'a set"
   Collect       :: "('a => bool) => 'a set"               (*comprehension*)
   Compl         :: "('a set) => 'a set"                   (*complement*)
   Int           :: "['a set, 'a set] => 'a set"       (infixl 70)
@@ -27,23 +26,20 @@
   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*)
-  Pow           :: "'a set => 'a set set"		  (*powerset*)
+  Pow           :: "'a set => 'a set set"                 (*powerset*)
   range         :: "('a => 'b) => 'b set"                 (*of function*)
   Ball, Bex     :: "['a set, 'a => bool] => bool"         (*bounded quantifiers*)
   inj, surj     :: "('a => 'b) => bool"                   (*inj/surjective*)
   inj_onto      :: "['a => 'b, 'a set] => bool"
   "``"          :: "['a => 'b, 'a set] => ('b set)"   (infixl 90)
   ":"           :: "['a, 'a set] => bool"             (infixl 50) (*membership*)
-  "~:"          :: "['a, 'a set] => bool"             ("(_ ~:/ _)" [50, 51] 50)
-
-  (* Finite Sets *)
-
-  insert        :: "['a, 'a set] => 'a set"
-  "{}"          :: "'a set"                           ("{}")
-  "@Finset"     :: "args => 'a set"                   ("{(_)}")
 
 
-  (** Binding Constants **)
+syntax
+
+  "~:"          :: "['a, 'a set] => bool"             (infixl 50)
+
+  "@Finset"     :: "args => 'a set"                   ("{(_)}")
 
   "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})")
   "@SetCompr"   :: "['a, idts, bool] => 'a set"       ("(1{_ |/_./ _})")
@@ -60,7 +56,6 @@
   "*Ball"       :: "[idt, 'a set, bool] => bool"      ("(3ALL _:_./ _)" 10)
   "*Bex"        :: "[idt, 'a set, bool] => bool"      ("(3EX _:_./ _)" 10)
 
-
 translations
   "x ~: y"      == "~ (x : y)"
   "{x, xs}"     == "insert(x, {xs})"
@@ -89,14 +84,14 @@
   Compl_def     "Compl(A)       == {x. ~x:A}"
   Un_def        "A Un B         == {x.x:A | x:B}"
   Int_def       "A Int B        == {x.x:A & x:B}"
-  set_diff_def  "A-B            == {x. x:A & ~x:B}"
+  set_diff_def  "A - B          == {x. x:A & ~x:B}"
   INTER_def     "INTER(A, B)    == {y. ! x:A. y: B(x)}"
   UNION_def     "UNION(A, B)    == {y. ? x:A. y: B(x)}"
   INTER1_def    "INTER1(B)      == INTER({x.True}, B)"
   UNION1_def    "UNION1(B)      == UNION({x.True}, B)"
   Inter_def     "Inter(S)       == (INT x:S. x)"
   Union_def     "Union(S)       == (UN x:S. x)"
-  Pow_def	"Pow(A)         == {B. B <= A}"
+  Pow_def       "Pow(A)         == {B. B <= A}"
   empty_def     "{}             == {x. False}"
   insert_def    "insert(a, B)   == {x.x=a} Un B"
   range_def     "range(f)       == {y. ? x. y=f(x)}"
@@ -113,18 +108,16 @@
 
 (* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P} *)
 
-fun dummyC(s) = Const(s,dummyT);
-
 val ex_tr = snd(mk_binder_tr("? ","Ex"));
 
 fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
   | nvars(_) = 1;
 
 fun setcompr_tr[e,idts,b] =
-  let val eq = dummyC("op =") $ Bound(nvars(idts)) $ e
-      val P = dummyC("op &") $ eq $ b
+  let val eq = Syntax.const("op =") $ Bound(nvars(idts)) $ e
+      val P = Syntax.const("op &") $ eq $ b
       val exP = ex_tr [idts,P]
-  in dummyC("Collect") $ Abs("",dummyT,exP) end;
+  in Syntax.const("Collect") $ Abs("",dummyT,exP) end;
 
 val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
 
@@ -135,14 +128,13 @@
 
       fun tr'(_ $ abs) =
         let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
-        in dummyC("@SetCompr") $ e $ idts $ Q end
+        in Syntax.const("@SetCompr") $ e $ idts $ Q end
   in ok(P,0); tr'(P) end;
 
 in
 
-val parse_translation = [("@SetCompr",setcompr_tr)];
-val print_translation = [("Collect",setcompr_tr')];
-
+val parse_translation = [("@SetCompr", setcompr_tr)];
+val print_translation = [("Collect", setcompr_tr')];
 val print_ast_translation =
   map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];