# HG changeset patch
# User haftmann
# Date 1228139768 -3600
# Node ID 08004ce1b16773c12f5e206bab6df98e1e7ef7e1
# Parent  7e631979922fcd9c72790f811ed3091483ca9647
added code equation for subset

diff -r 7e631979922f -r 08004ce1b167 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Mon Dec 01 13:43:32 2008 +0100
+++ b/src/HOL/Library/Executable_Set.thy	Mon Dec 01 14:56:08 2008 +0100
@@ -16,7 +16,7 @@
 
 declare subset_def [symmetric, code unfold]
 
-lemma "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
+lemma [code]: "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   unfolding subset_def subset_eq ..
 
 definition is_empty :: "'a set \<Rightarrow> bool" where
@@ -32,8 +32,7 @@
   "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
   unfolding bex_triv_one_point1 ..
 
-definition
-  filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   "filter_set P xs = {x\<in>xs. P x}"