# HG changeset patch
# User bulwahn
# Date 1328173950 -3600
# Node ID da32cf32c0c799bf5f9d575bae1f0d6e58f9e22a
# Parent  f56be74d7f51d8b3a51dc99c4e6425f6a57414f2
adding a minimally refined equality on sets for code generation

diff -r f56be74d7f51 -r da32cf32c0c7 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Feb 02 10:12:11 2012 +0100
+++ b/src/HOL/List.thy	Thu Feb 02 10:12:30 2012 +0100
@@ -5676,6 +5676,11 @@
 
 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)
+
 lemma setsum_code [code]:
   "setsum f (set xs) = listsum (map f (remdups xs))"
 by (simp add: listsum_distinct_conv_setsum_set)