# HG changeset patch
# User wenzelm
# Date 751556187 -3600
# Node ID 201061643c4b0f44a45038554e86b1b211604fb1
# Parent  fc1674026e2038956504ca0f87624d52fa18f33f
added white-space;
made ~: a fake infix;

diff -r fc1674026e20 -r 201061643c4b Set.thy
--- a/Set.thy	Mon Oct 25 14:35:17 1993 +0100
+++ b/Set.thy	Mon Oct 25 14:36:27 1993 +0100
@@ -19,20 +19,21 @@
 
   (* 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"                 (*inj/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"                   (*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 => 'b, 'a set] => ('b set)"   (infixl 90)
+  ":"           :: "['a, 'a set] => bool"             (infixl 50) (*membership*)
+  "~:"          :: "['a, 'a set] => bool"             ("(_ ~:/ _)" [50, 51] 50)
 
   (* Finite Sets *)
 
@@ -43,7 +44,7 @@
 
   (** Binding Constants **)
 
-  "@Coll"       :: "[idt, bool] => 'a set"   ("(1{_./ _})")  (*collection*)
+  "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})") (*collection*)
 
   (* Big Intersection / Union *)
 
@@ -59,6 +60,9 @@
 
 
 translations
+  "x ~: y"      == "~ (x : y)"
+  "{x, xs}"     == "insert(x, {xs})"
+  "{x}"         == "insert(x, {})"
   "{x. P}"      == "Collect(%x. P)"
   "INT x:A. B"  == "INTER(A, %x. B)"
   "UN x:A. B"   == "UNION(A, %x. B)"
@@ -67,11 +71,6 @@
   "ALL x:A. P"  => "Ball(A, %x. P)"
   "EX x:A. P"   => "Bex(A, %x. P)"
 
-  "x ~: y"      == "~ (x:y)"
-
-  "{x, xs}"     == "insert(x, {xs})"
-  "{x}"         == "insert(x, {})"
-
 
 rules
 
diff -r fc1674026e20 -r 201061643c4b set.thy
--- a/set.thy	Mon Oct 25 14:35:17 1993 +0100
+++ b/set.thy	Mon Oct 25 14:36:27 1993 +0100
@@ -19,20 +19,21 @@
 
   (* 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"                 (*inj/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"                   (*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 => 'b, 'a set] => ('b set)"   (infixl 90)
+  ":"           :: "['a, 'a set] => bool"             (infixl 50) (*membership*)
+  "~:"          :: "['a, 'a set] => bool"             ("(_ ~:/ _)" [50, 51] 50)
 
   (* Finite Sets *)
 
@@ -43,7 +44,7 @@
 
   (** Binding Constants **)
 
-  "@Coll"       :: "[idt, bool] => 'a set"   ("(1{_./ _})")  (*collection*)
+  "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})") (*collection*)
 
   (* Big Intersection / Union *)
 
@@ -59,6 +60,9 @@
 
 
 translations
+  "x ~: y"      == "~ (x : y)"
+  "{x, xs}"     == "insert(x, {xs})"
+  "{x}"         == "insert(x, {})"
   "{x. P}"      == "Collect(%x. P)"
   "INT x:A. B"  == "INTER(A, %x. B)"
   "UN x:A. B"   == "UNION(A, %x. B)"
@@ -67,11 +71,6 @@
   "ALL x:A. P"  => "Ball(A, %x. P)"
   "EX x:A. P"   => "Bex(A, %x. P)"
 
-  "x ~: y"      == "~ (x:y)"
-
-  "{x, xs}"     == "insert(x, {xs})"
-  "{x}"         == "insert(x, {})"
-
 
 rules