--- a/src/HOL/Set.thy Thu Mar 23 18:14:06 2006 +0100
+++ b/src/HOL/Set.thy Thu Mar 23 20:03:53 2006 +0100
@@ -47,9 +47,11 @@
subsection {* Additional concrete syntax *}
+abbreviation (output)
+ range :: "('a => 'b) => 'b set" -- "of function"
+ "range f = f ` UNIV"
+
syntax
- range :: "('a => 'b) => 'b set" -- "of function"
-
"op ~:" :: "'a => 'a set => bool" ("op ~:") -- "non-membership"
"op ~:" :: "'a => 'a set => bool" ("(_/ ~: _)" [50, 51] 50)
@@ -72,7 +74,6 @@
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10)
translations
- "range f" == "f`UNIV"
"x ~: y" == "~ (x : y)"
"{x, xs}" == "insert x {xs}"
"{x}" == "insert x {}"