src/HOL/Set.thy

--- a/src/HOL/Set.thy	Tue Jul 28 13:37:08 2009 +0200
+++ b/src/HOL/Set.thy	Tue Jul 28 13:37:09 2009 +0200
@@ -100,8 +100,8 @@
 
 text {* Set enumerations *}
 
-definition empty :: "'a set" ("{}") where
-  bot_set_eq [symmetric]: "{} = bot"
+abbreviation empty :: "'a set" ("{}") where
+  "{} \<equiv> bot"
 
 definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
@@ -541,12 +541,12 @@
 
 subsubsection {* The universal set -- UNIV *}
 
-definition UNIV :: "'a set" where
-  top_set_eq [symmetric]: "UNIV = top"
+abbreviation UNIV :: "'a set" where
+  "UNIV \<equiv> top"
 
 lemma UNIV_def:
   "UNIV = {x. True}"
-  by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq Collect_def)
+  by (simp add: top_fun_eq top_bool_eq Collect_def)
 
 lemma UNIV_I [simp]: "x : UNIV"
   by (simp add: UNIV_def)
@@ -579,7 +579,7 @@
 
 lemma empty_def:
   "{} = {x. False}"
-  by (simp add: bot_set_eq [symmetric] bot_fun_eq bot_bool_eq Collect_def)
+  by (simp add: bot_fun_eq bot_bool_eq Collect_def)
 
 lemma empty_iff [simp]: "(c : {}) = False"
   by (simp add: empty_def)