1.1 --- a/src/HOL/Set.thy	Fri Sep 18 14:09:38 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Sat Sep 19 07:38:03 2009 +0200
     1.3 @@ -652,8 +652,8 @@
     1.4  
     1.5  subsubsection {* Binary union -- Un *}
     1.6  
     1.7 -definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
     1.8 -  sup_set_eq [symmetric]: "A Un B = sup A B"
     1.9 +abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
    1.10 +  "op Un \<equiv> sup"
    1.11  
    1.12  notation (xsymbols)
    1.13    union  (infixl "\<union>" 65)
    1.14 @@ -663,7 +663,7 @@
    1.15  
    1.16  lemma Un_def:
    1.17    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
    1.18 -  by (simp add: sup_fun_eq sup_bool_eq sup_set_eq [symmetric] Collect_def mem_def)
    1.19 +  by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
    1.20  
    1.21  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
    1.22    by (unfold Un_def) blast
    1.23 @@ -689,15 +689,13 @@
    1.24    by (simp add: Collect_def mem_def insert_compr Un_def)
    1.25  
    1.26  lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
    1.27 -  apply (fold sup_set_eq)
    1.28 -  apply (erule mono_sup)
    1.29 -  done
    1.30 +  by (fact mono_sup)
    1.31  
    1.32  
    1.33  subsubsection {* Binary intersection -- Int *}
    1.34  
    1.35 -definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    1.36 -  inf_set_eq [symmetric]: "A Int B = inf A B"
    1.37 +abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
    1.38 +  "op Int \<equiv> inf"
    1.39  
    1.40  notation (xsymbols)
    1.41    inter  (infixl "\<inter>" 70)
    1.42 @@ -707,7 +705,7 @@
    1.43  
    1.44  lemma Int_def:
    1.45    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
    1.46 -  by (simp add: inf_fun_eq inf_bool_eq inf_set_eq [symmetric] Collect_def mem_def)
    1.47 +  by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
    1.48  
    1.49  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
    1.50    by (unfold Int_def) blast
    1.51 @@ -725,9 +723,7 @@
    1.52    by simp
    1.53  
    1.54  lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
    1.55 -  apply (fold inf_set_eq)
    1.56 -  apply (erule mono_inf)
    1.57 -  done
    1.58 +  by (fact mono_inf)
    1.59  
    1.60  
    1.61  subsubsection {* Set difference *}