src/HOL/IsaMakefile

 
 HOL-Library: HOL $(LOG)/HOL-Library.gz
 
 $(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 \
   Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
   Library/Nat_Infinity.thy Library/Word.thy \

 
 ## HOL-MicroJava
 
 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 \
   MicroJava/Comp/CorrCompTp.thy \
   MicroJava/Comp/DefsComp.thy \

 
 ## HOL-Extraction
 
 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 \
   Extraction/document/root.bib
 	@$(ISATOOL) usedir $(OUT)/HOL Extraction