src/HOL/Set.thy

--- a/src/HOL/Set.thy	Fri Sep 18 14:09:38 2009 +0200
+++ b/src/HOL/Set.thy	Sat Sep 19 07:38:03 2009 +0200
@@ -652,8 +652,8 @@
 
 subsubsection {* Binary union -- Un *}
 
-definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
-  sup_set_eq [symmetric]: "A Un B = sup A B"
+abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
+  "op Un \<equiv> sup"
 
 notation (xsymbols)
   union  (infixl "\<union>" 65)
@@ -663,7 +663,7 @@
 
 lemma Un_def:
   "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
-  by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
+  by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
 
 lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
   by (unfold Un_def) blast
@@ -689,15 +689,13 @@
   by (simp add: Collect_def mem_def insert_compr Un_def)
 
 lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
-  apply (fold sup_set_eq)
-  apply (erule mono_sup)
-  done
+  by (fact mono_sup)
 
 
 subsubsection {* Binary intersection -- Int *}
 
-definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
-  inf_set_eq [symmetric]: "A Int B = inf A B"
+abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
+  "op Int \<equiv> inf"
 
 notation (xsymbols)
   inter  (infixl "\<inter>" 70)
@@ -707,7 +705,7 @@
 
 lemma Int_def:
   "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
-  by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
+  by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
 
 lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   by (unfold Int_def) blast
@@ -725,9 +723,7 @@
   by simp
 
 lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
-  apply (fold inf_set_eq)
-  apply (erule mono_inf)
-  done
+  by (fact mono_inf)
 
 
 subsubsection {* Set difference *}