src/HOL/Library/AList_Mapping.thy
changeset 44913 48240fb48980
parent 44897 787983a08bfb
child 45873 37ffb8797a63
     1.1 --- a/src/HOL/Library/AList_Mapping.thy	Tue Sep 13 09:25:19 2011 +0200
     1.2 +++ b/src/HOL/Library/AList_Mapping.thy	Tue Sep 13 09:28:03 2011 +0200
     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 @@ -69,4 +69,4 @@
    1.13    "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
    1.14    by (fact equal_refl)
    1.15    
    1.16 -end
    1.17 \ No newline at end of file
    1.18 +end