src/HOL/Library/AList_Mapping.thy
changeset 45873 37ffb8797a63
parent 44913 48240fb48980
child 46171 19f68d7671f0
     1.1 --- a/src/HOL/Library/AList_Mapping.thy	Wed Dec 14 16:30:30 2011 +0100
     1.2 +++ b/src/HOL/Library/AList_Mapping.thy	Wed Dec 14 16:30:32 2011 +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 Mapping
     1.8 +imports AList_Impl Mapping
     1.9  begin
    1.10  
    1.11  definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where