src/HOL/Library/AList_Mapping.thy
changeset 46238 9ace9e5b79be
parent 46171 19f68d7671f0
child 49929 70300f1b6835
     1.1 --- a/src/HOL/Library/AList_Mapping.thy	Tue Jan 17 09:38:30 2012 +0100
     1.2 +++ b/src/HOL/Library/AList_Mapping.thy	Tue Jan 17 10:45:42 2012 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Implementation of mappings with Association Lists *}
     1.5  
     1.6  theory AList_Mapping
     1.7 -imports AList_Impl Mapping
     1.8 +imports AList Mapping
     1.9  begin
    1.10  
    1.11  definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
    1.12 @@ -30,11 +30,11 @@
    1.13    by (cases xs) (simp_all add: is_empty_def null_def)
    1.14  
    1.15  lemma update_Mapping [code]:
    1.16 -  "Mapping.update k v (Mapping xs) = Mapping (AList_Impl.update k v xs)"
    1.17 +  "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
    1.18    by (rule mapping_eqI) (simp add: update_conv')
    1.19  
    1.20  lemma delete_Mapping [code]:
    1.21 -  "Mapping.delete k (Mapping xs) = Mapping (AList_Impl.delete k xs)"
    1.22 +  "Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)"
    1.23    by (rule mapping_eqI) (simp add: delete_conv')
    1.24  
    1.25  lemma ordered_keys_Mapping [code]: