src/HOL/IsaMakefile
changeset 23854 688a8a7bcd4e
parent 23772 b96db2903a9a
child 23882 83b0f2518380
--- 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 \