--- a/src/HOL/IsaMakefile Tue Sep 13 09:25:19 2011 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 13 09:28:03 2011 +0200
@@ -430,7 +430,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_Impl.thy Library/AList_Mapping.thy \
+ Library/AList.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 \
--- a/src/HOL/Library/AList.thy Tue Sep 13 09:25:19 2011 +0200
+++ b/src/HOL/Library/AList.thy Tue Sep 13 09:28:03 2011 +0200
@@ -1,10 +1,10 @@
-(* Title: HOL/Library/AList_Impl.thy
+(* Title: HOL/Library/AList.thy
Author: Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
*)
header {* Implementation of Association Lists *}
-theory AList_Impl
+theory AList
imports Main More_List
begin
--- a/src/HOL/Library/AList_Mapping.thy Tue Sep 13 09:25:19 2011 +0200
+++ b/src/HOL/Library/AList_Mapping.thy Tue Sep 13 09:28:03 2011 +0200
@@ -5,7 +5,7 @@
header {* Implementation of mappings with Association Lists *}
theory AList_Mapping
-imports AList_Impl Mapping
+imports AList Mapping
begin
definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
@@ -69,4 +69,4 @@
"HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
by (fact equal_refl)
-end
\ No newline at end of file
+end