# HG changeset patch # User bulwahn # Date 1323876632 -3600 # Node ID 37ffb8797a6398b608f457b0caf70de50e665146 # Parent 3759fb8a02b81cd530c67b4186a1c4b55a2b71d5 correcting dependencies after renaming diff -r 3759fb8a02b8 -r 37ffb8797a63 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Dec 14 16:30:30 2011 +0100 +++ b/src/HOL/IsaMakefile Wed Dec 14 16:30:32 2011 +0100 @@ -435,7 +435,7 @@ $(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML \ $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \ Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \ - Library/AList.thy Library/AList_Mapping.thy \ + Library/AList_Impl.thy Library/AList_Mapping.thy \ Library/BigO.thy Library/Binomial.thy \ Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \ Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \ diff -r 3759fb8a02b8 -r 37ffb8797a63 src/HOL/Library/AList_Mapping.thy --- a/src/HOL/Library/AList_Mapping.thy Wed Dec 14 16:30:30 2011 +0100 +++ b/src/HOL/Library/AList_Mapping.thy Wed Dec 14 16:30:32 2011 +0100 @@ -5,7 +5,7 @@ header {* Implementation of mappings with Association Lists *} theory AList_Mapping -imports AList Mapping +imports AList_Impl Mapping begin definition Mapping :: "('a \ 'b) list \ ('a, 'b) mapping" where