src/HOL/Set.thy

 
 lemma subsetCE [no_atp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   -- {* Classical elimination rule. *}
   by (auto simp add: less_eq_set_def le_fun_def)
 
-lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
+lemma subset_eq [code, no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
 
 lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   by blast
 
 lemma subset_refl: "A \<subseteq> A"

 
 
 subsubsection {* Operations for execution *}
 
 definition is_empty :: "'a set \<Rightarrow> bool" where
-  "is_empty A \<longleftrightarrow> A = {}"
+  [code_abbrev]: "is_empty A \<longleftrightarrow> A = {}"
 
 hide_const (open) is_empty
 
 definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  "remove x A = A - {x}"
+  [code_abbrev]: "remove x A = A - {x}"
 
 hide_const (open) remove
 
 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   [code_abbrev]: "project P A = {a \<in> A. P a}"

 
 instance proof
 qed (auto simp add: equal_set_def)
 
 end
+
 
 text {* Misc *}
 
 hide_const (open) member not_member