correcting theory name and dependencies
authorbulwahn
Tue Sep 13 09:28:03 2011 +0200 (2011-09-13)
changeset 4491348240fb48980
parent 44912 23956688856e
child 44914 f0fd38929d21
correcting theory name and dependencies
src/HOL/IsaMakefile
src/HOL/Library/AList.thy
src/HOL/Library/AList_Mapping.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Sep 13 09:25:19 2011 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Sep 13 09:28:03 2011 +0200
     1.3 @@ -430,7 +430,7 @@
     1.4  $(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML				\
     1.5    $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
     1.6    Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
     1.7 -  Library/AList_Impl.thy Library/AList_Mapping.thy 			\
     1.8 +  Library/AList.thy Library/AList_Mapping.thy 				\
     1.9    Library/BigO.thy Library/Binomial.thy 				\
    1.10    Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
    1.11    Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
     2.1 --- a/src/HOL/Library/AList.thy	Tue Sep 13 09:25:19 2011 +0200
     2.2 +++ b/src/HOL/Library/AList.thy	Tue Sep 13 09:28:03 2011 +0200
     2.3 @@ -1,10 +1,10 @@
     2.4 -(*  Title:      HOL/Library/AList_Impl.thy
     2.5 +(*  Title:      HOL/Library/AList.thy
     2.6      Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser, TU Muenchen
     2.7  *)
     2.8  
     2.9  header {* Implementation of Association Lists *}
    2.10  
    2.11 -theory AList_Impl 
    2.12 +theory AList
    2.13  imports Main More_List
    2.14  begin
    2.15  
     3.1 --- a/src/HOL/Library/AList_Mapping.thy	Tue Sep 13 09:25:19 2011 +0200
     3.2 +++ b/src/HOL/Library/AList_Mapping.thy	Tue Sep 13 09:28:03 2011 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Implementation of mappings with Association Lists *}
     3.5  
     3.6  theory AList_Mapping
     3.7 -imports AList_Impl Mapping
     3.8 +imports AList Mapping
     3.9  begin
    3.10  
    3.11  definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
    3.12 @@ -69,4 +69,4 @@
    3.13    "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
    3.14    by (fact equal_refl)
    3.15    
    3.16 -end
    3.17 \ No newline at end of file
    3.18 +end