--- a/src/HOL/IsaMakefile Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/IsaMakefile Thu Jul 19 21:47:39 2007 +0200
@@ -201,10 +201,9 @@
$(LOG)/HOL-Library.gz: $(OUT)/HOL \
Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
- Library/EfficientNat.thy Library/ExecutableSet.thy \
- Library/ExecutableRat.thy \
- Library/Executable_Real.thy \
- Library/MLString.thy Library/Infinite_Set.thy \
+ Library/Efficient_Nat.thy Library/Executable_Set.thy \
+ Library/Executable_Rat.thy Library/Executable_Real.thy \
+ Library/ML_Int.thy Library/ML_String.thy Library/Infinite_Set.thy \
Library/FuncSet.thy Library/Library.thy \
Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \
Library/NatPair.thy \
@@ -538,7 +537,7 @@
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
-$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/ExecutableSet.thy \
+$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy \
MicroJava/ROOT.ML \
MicroJava/Comp/AuxLemmas.thy \
MicroJava/Comp/CorrComp.thy \
@@ -604,7 +603,7 @@
HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
-$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/EfficientNat.thy \
+$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/Efficient_Nat.thy \
Extraction/Higman.thy Extraction/ROOT.ML Extraction/Pigeonhole.thy \
Extraction/QuotRem.thy \
Extraction/Warshall.thy Extraction/document/root.tex \