src/HOL/Set.thy
changeset 41076 a7fba340058c
parent 40872 7c556a9240de
child 41082 9ff94e7cc3b3
     1.1 --- a/src/HOL/Set.thy	Wed Dec 08 13:34:50 2010 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Dec 08 13:34:51 2010 +0100
     1.3 @@ -540,7 +540,7 @@
     1.4  
     1.5  lemma UNIV_def:
     1.6    "UNIV = {x. True}"
     1.7 -  by (simp add: top_fun_eq top_bool_eq Collect_def)
     1.8 +  by (simp add: top_fun_def top_bool_def Collect_def)
     1.9  
    1.10  lemma UNIV_I [simp]: "x : UNIV"
    1.11    by (simp add: UNIV_def)
    1.12 @@ -573,7 +573,7 @@
    1.13  
    1.14  lemma empty_def:
    1.15    "{} = {x. False}"
    1.16 -  by (simp add: bot_fun_eq bot_bool_eq Collect_def)
    1.17 +  by (simp add: bot_fun_def bot_bool_def Collect_def)
    1.18  
    1.19  lemma empty_iff [simp]: "(c : {}) = False"
    1.20    by (simp add: empty_def)
    1.21 @@ -625,6 +625,7 @@
    1.22  lemma Pow_not_empty: "Pow A \<noteq> {}"
    1.23    using Pow_top by blast
    1.24  
    1.25 +
    1.26  subsubsection {* Set complement *}
    1.27  
    1.28  lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
    1.29 @@ -649,7 +650,7 @@
    1.30  subsubsection {* Binary union -- Un *}
    1.31  
    1.32  abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
    1.33 -  "op Un \<equiv> sup"
    1.34 +  "union \<equiv> sup"
    1.35  
    1.36  notation (xsymbols)
    1.37    union  (infixl "\<union>" 65)
    1.38 @@ -659,7 +660,7 @@
    1.39  
    1.40  lemma Un_def:
    1.41    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
    1.42 -  by (simp add: sup_fun_eq sup_bool_eq Collect_def mem_def)
    1.43 +  by (simp add: sup_fun_def sup_bool_def Collect_def mem_def)
    1.44  
    1.45  lemma Un_iff [simp]: "(c : A Un B) = (c:A | c:B)"
    1.46    by (unfold Un_def) blast
    1.47 @@ -701,7 +702,7 @@
    1.48  
    1.49  lemma Int_def:
    1.50    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
    1.51 -  by (simp add: inf_fun_eq inf_bool_eq Collect_def mem_def)
    1.52 +  by (simp add: inf_fun_def inf_bool_def Collect_def mem_def)
    1.53  
    1.54  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
    1.55    by (unfold Int_def) blast