src/HOL/Set.thy
changeset 32264 0be31453f698
parent 32139 e271a64f03ff
child 32456 341c83339aeb
     1.1 --- a/src/HOL/Set.thy	Tue Jul 28 13:37:08 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Jul 28 13:37:09 2009 +0200
     1.3 @@ -100,8 +100,8 @@
     1.4  
     1.5  text {* Set enumerations *}
     1.6  
     1.7 -definition empty :: "'a set" ("{}") where
     1.8 -  bot_set_eq [symmetric]: "{} = bot"
     1.9 +abbreviation empty :: "'a set" ("{}") where
    1.10 +  "{} \<equiv> bot"
    1.11  
    1.12  definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.13    insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
    1.14 @@ -541,12 +541,12 @@
    1.15  
    1.16  subsubsection {* The universal set -- UNIV *}
    1.17  
    1.18 -definition UNIV :: "'a set" where
    1.19 -  top_set_eq [symmetric]: "UNIV = top"
    1.20 +abbreviation UNIV :: "'a set" where
    1.21 +  "UNIV \<equiv> top"
    1.22  
    1.23  lemma UNIV_def:
    1.24    "UNIV = {x. True}"
    1.25 -  by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq Collect_def)
    1.26 +  by (simp add: top_fun_eq top_bool_eq Collect_def)
    1.27  
    1.28  lemma UNIV_I [simp]: "x : UNIV"
    1.29    by (simp add: UNIV_def)
    1.30 @@ -579,7 +579,7 @@
    1.31  
    1.32  lemma empty_def:
    1.33    "{} = {x. False}"
    1.34 -  by (simp add: bot_set_eq [symmetric] bot_fun_eq bot_bool_eq Collect_def)
    1.35 +  by (simp add: bot_fun_eq bot_bool_eq Collect_def)
    1.36  
    1.37  lemma empty_iff [simp]: "(c : {}) = False"
    1.38    by (simp add: empty_def)