# HG changeset patch
# User bulwahn
# Date 1315898883 -7200
# Node ID 48240fb48980a90342011a3c4350203f48f90ad3
# Parent  23956688856ea88110e3c2824d3b030d7d65bcb7
correcting theory name and dependencies

diff -r 23956688856e -r 48240fb48980 src/HOL/IsaMakefile
--- 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	\
diff -r 23956688856e -r 48240fb48980 src/HOL/Library/AList.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
 
diff -r 23956688856e -r 48240fb48980 src/HOL/Library/AList_Mapping.thy
--- 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