# HG changeset patch
# User berghofe
# Date 1210150769 -7200
# Node ID e82229ee8f43e819dae92b542b6595dabe3dfd78
# Parent  0cb35f537c91a389912c86050fd5144f0c5f9647
- Declared subset_eq as code lemma
- Deleted types_code declaration for sets

diff -r 0cb35f537c91 -r e82229ee8f43 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Wed May 07 10:59:27 2008 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Wed May 07 10:59:29 2008 +0200
@@ -15,6 +15,8 @@
   "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   by blast
 
+declare subset_eq [code]
+
 lemma [code]:
   "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
   unfolding bex_triv_one_point1 ..
@@ -64,7 +66,7 @@
 
 lemma member_nil [simp]:
   "member [] = (\<lambda>x. False)"
-proof
+proof (rule ext)
   fix x
   show "member [] x = False" unfolding member_def by simp
 qed
@@ -240,30 +242,6 @@
 nonfix subset;
 *}
 
-subsubsection {* type serializations *}
-
-types_code
-  set ("_ list")
-attach (term_of) {*
-fun term_of_set f T [] = Const ("{}", Type ("set", [T]))
-  | term_of_set f T (x :: xs) = Const ("insert",
-      T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs;
-*}
-attach (test) {*
-fun gen_set' aG aT i j = frequency
-  [(i, fn () =>
-      let
-        val (x, t) = aG j;
-        val (xs, ts) = gen_set' aG aT (i-1) j
-      in
-        (x :: xs, fn () => Const ("insert",
-           aT --> Type ("set", [aT]) --> Type ("set", [aT])) $ t () $ ts ())
-      end),
-   (1, fn () => ([], fn () => Const ("{}", Type ("set", [aT]))))] ()
-and gen_set aG aT i = gen_set' aG aT i i;
-*}
-
-
 subsubsection {* const serializations *}
 
 consts_code