--- 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