# HG changeset patch
# User bulwahn
# Date 1332921742 -7200
# Node ID 2ae2b6fa9c84f523d152ca3c69c040b41d35189c
# Parent  2fa00264392a1a5dfde0f232f1a11874c351f776
removing now redundant impl_of theorems in DAList

diff -r 2fa00264392a -r 2ae2b6fa9c84 src/HOL/Library/DAList.thy
--- a/src/HOL/Library/DAList.thy	Wed Mar 28 10:00:52 2012 +0200
+++ b/src/HOL/Library/DAList.thy	Wed Mar 28 10:02:22 2012 +0200
@@ -68,17 +68,6 @@
 where "map_default" is "AList.map_default :: 'key => 'value => ('value => 'value) => ('key * 'value) list => ('key * 'value) list"
 by (simp add: distinct_map_default)
 
-(* FIXME: theorems are still used in Multiset; make code certificates available to the user *)
-lemma impl_of_empty: "impl_of empty = []"
-by (simp add: empty_def Alist_inverse)
-
-lemma impl_of_update: "impl_of (update k v xs) = AList.update k v (impl_of xs)"
-by (simp add: update_def Alist_inverse distinct_update)
-
-lemma impl_of_filter:
-  "impl_of (filter P xs) = List.filter P (impl_of xs)"
-unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter)
-
 subsection {* Abstract operation properties *}
 
 (* FIXME: to be completed *)