src/HOL/Library/AList_Mapping.thy
changeset 46171 19f68d7671f0
parent 45873 37ffb8797a63
child 46238 9ace9e5b79be
     1.1 --- a/src/HOL/Library/AList_Mapping.thy	Tue Jan 10 10:48:39 2012 +0100
     1.2 +++ b/src/HOL/Library/AList_Mapping.thy	Tue Jan 10 15:48:10 2012 +0100
     1.3 @@ -30,11 +30,11 @@
     1.4    by (cases xs) (simp_all add: is_empty_def null_def)
     1.5  
     1.6  lemma update_Mapping [code]:
     1.7 -  "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
     1.8 +  "Mapping.update k v (Mapping xs) = Mapping (AList_Impl.update k v xs)"
     1.9    by (rule mapping_eqI) (simp add: update_conv')
    1.10  
    1.11  lemma delete_Mapping [code]:
    1.12 -  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
    1.13 +  "Mapping.delete k (Mapping xs) = Mapping (AList_Impl.delete k xs)"
    1.14    by (rule mapping_eqI) (simp add: delete_conv')
    1.15  
    1.16  lemma ordered_keys_Mapping [code]: