1.1 --- a/src/HOL/Set.thy	Thu Jan 05 20:26:01 2012 +0100
     1.2 +++ b/src/HOL/Set.thy	Sun Jan 01 11:28:45 2012 +0100
     1.3 @@ -508,7 +508,7 @@
     1.4    -- {* Classical elimination rule. *}
     1.5    by (auto simp add: less_eq_set_def le_fun_def)
     1.6  
     1.7 -lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
     1.8 +lemma subset_eq [code, no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
     1.9  
    1.10  lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
    1.11    by blast
    1.12 @@ -1810,12 +1810,12 @@
    1.13  subsubsection {* Operations for execution *}
    1.14  
    1.15  definition is_empty :: "'a set \<Rightarrow> bool" where
    1.16 -  "is_empty A \<longleftrightarrow> A = {}"
    1.17 +  [code_abbrev]: "is_empty A \<longleftrightarrow> A = {}"
    1.18  
    1.19  hide_const (open) is_empty
    1.20  
    1.21  definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.22 -  "remove x A = A - {x}"
    1.23 +  [code_abbrev]: "remove x A = A - {x}"
    1.24  
    1.25  hide_const (open) remove
    1.26  
    1.27 @@ -1835,6 +1835,7 @@
    1.28  
    1.29  end
    1.30  
    1.31 +
    1.32  text {* Misc *}
    1.33  
    1.34  hide_const (open) member not_member