src/HOL/Library/DAList.thy
changeset 47178 2ae2b6fa9c84
parent 47143 212f7a975d49
child 47308 9caab698dbe4
     1.1 --- a/src/HOL/Library/DAList.thy	Wed Mar 28 10:00:52 2012 +0200
     1.2 +++ b/src/HOL/Library/DAList.thy	Wed Mar 28 10:02:22 2012 +0200
     1.3 @@ -68,17 +68,6 @@
     1.4  where "map_default" is "AList.map_default :: 'key => 'value => ('value => 'value) => ('key * 'value) list => ('key * 'value) list"
     1.5  by (simp add: distinct_map_default)
     1.6  
     1.7 -(* FIXME: theorems are still used in Multiset; make code certificates available to the user *)
     1.8 -lemma impl_of_empty: "impl_of empty = []"
     1.9 -by (simp add: empty_def Alist_inverse)
    1.10 -
    1.11 -lemma impl_of_update: "impl_of (update k v xs) = AList.update k v (impl_of xs)"
    1.12 -by (simp add: update_def Alist_inverse distinct_update)
    1.13 -
    1.14 -lemma impl_of_filter:
    1.15 -  "impl_of (filter P xs) = List.filter P (impl_of xs)"
    1.16 -unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter)
    1.17 -
    1.18  subsection {* Abstract operation properties *}
    1.19  
    1.20  (* FIXME: to be completed *)