diff -r 2d399a776de2 -r c9e50153e5ae src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Dec 26 17:40:43 2011 +0100
+++ b/src/HOL/Set.thy	Mon Dec 26 18:32:43 2011 +0100
@@ -1791,6 +1791,34 @@
 hide_const (open) bind
 
 
+subsubsection {* Operations for execution *}
+
+definition is_empty :: "'a set \<Rightarrow> bool" where
+  "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}"
+
+hide_const (open) remove
+
+definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+  "project P A = {a \<in> A. P a}"
+
+hide_const (open) project
+
+instantiation set :: (equal) equal
+begin
+
+definition
+  "HOL.equal A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
+
+instance proof
+qed (auto simp add: equal_set_def)
+
+end
+
 text {* Misc *}
 
 hide_const (open) member not_member