# HG changeset patch
# User bulwahn
# Date 1328106482 -3600
# Node ID 68f973ffd763141bd52e4303ad4af3665aea95b4
# Parent  69f2d19f7d332d122e9b32d3c1b4663d82f1cc99
improving code equations for multisets that violated the distinct AList abstraction

diff -r 69f2d19f7d33 -r 68f973ffd763 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Feb 02 01:55:17 2012 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Feb 01 15:28:02 2012 +0100
@@ -1175,12 +1175,12 @@
   by (simp add: Bag_def count_of_multiset Abs_multiset_inverse)
 
 lemma Mempty_Bag [code]:
-  "{#} = Bag (Alist [])"
-  by (simp add: multiset_eq_iff alist.Alist_inverse)
+  "{#} = Bag (DAList.empty)"
+  by (simp add: multiset_eq_iff alist.Alist_inverse DAList.empty_def)
   
 lemma single_Bag [code]:
-  "{#x#} = Bag (Alist [(x, 1)])"
-  by (simp add: multiset_eq_iff alist.Alist_inverse)
+  "{#x#} = Bag (DAList.update x 1 DAList.empty)"
+  by (simp add: multiset_eq_iff alist.Alist_inverse impl_of_update impl_of_empty)
 
 lemma union_Bag [code]:
   "Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)"