src/HOL/Set.thy
changeset 46127 af3b95160b59
parent 46036 6a86cc88b02f
child 46128 53e7cc599f58
--- a/src/HOL/Set.thy	Thu Jan 05 20:26:01 2012 +0100
+++ b/src/HOL/Set.thy	Sun Jan 01 11:28:45 2012 +0100
@@ -508,7 +508,7 @@
   -- {* 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
@@ -1810,12 +1810,12 @@
 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
 
@@ -1835,6 +1835,7 @@
 
 end
 
+
 text {* Misc *}
 
 hide_const (open) member not_member