--- a/Set.thy Mon Oct 04 15:43:54 1993 +0100
+++ b/Set.thy Thu Oct 07 10:20:30 1993 +0100
@@ -19,20 +19,20 @@
(* 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" (*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*)
(* Finite Sets *)
@@ -43,7 +43,7 @@
(** Binding Constants **)
- "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*)
+ "@Coll" :: "[idt, bool] => 'a set" ("(1{_./ _})") (*collection*)
(* Big Intersection / Union *)
@@ -67,6 +67,8 @@
"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, {})"