changeset 46396 | da32cf32c0c7 |
parent 46383 | 26c422552cfe |
child 46418 | 22bb415d7754 |
--- 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)