# HG changeset patch
# User bulwahn
# Date 1328426679 -3600
# Node ID 22bb415d7754a365a45919505181030bf29a6e99
# Parent  1a68fcb80b62c002971cf23f7ce65bdcee2e70b4
another try to improve code generation of set equality (cf. da32cf32c0c7)

diff -r 1a68fcb80b62 -r 22bb415d7754 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Feb 05 08:24:38 2012 +0100
+++ b/src/HOL/List.thy	Sun Feb 05 08:24:39 2012 +0100
@@ -5677,9 +5677,12 @@
 text {* Further operations on sets *}
 
 (* Minimal refinement of equality on sets *)
-lemma [code]:
-  "HOL.equal (set []) (List.coset []) = False"
-by (metis UNIV_coset UNIV_not_empty empty_set equal_eq)
+declare subset_eq[code del]
+lemma subset_code [code]:
+  "set xs <= B \<longleftrightarrow> (ALL x : set xs. x : B)"
+  "List.coset xs <= List.coset ys \<longleftrightarrow> set ys <= set xs"
+  "List.coset [] <= set [] \<longleftrightarrow> False"
+by auto
 
 lemma setsum_code [code]:
   "setsum f (set xs) = listsum (map f (remdups xs))"