src/HOL/IsaMakefile

   $(SRC)/Tools/code/code_funcgr.ML $(SRC)/Tools/code/code_name.ML	\
   $(SRC)/Tools/code/code_package.ML $(SRC)/Tools/code/code_target.ML	\
   $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML			\
   $(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy	\
   Accessible_Part.thy Arith_Tools.thy Code_Setup.thy Datatype.thy 			\
-  Dense_Linear_Order.thy Divides.thy Equiv_Relations.thy Extraction.thy	\
+  Divides.thy Equiv_Relations.thy Extraction.thy	\
   Finite_Set.thy Fun.thy FunDef.thy HOL.thy		\
   Hilbert_Choice.thy Inductive.thy Int.thy IntDiv.thy	\
   Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy	\
   OrderedGroup.thy Orderings.thy Power.thy PreList.thy	\
   Predicate.thy Product_Type.thy ROOT.ML Recdef.thy			\

 HOL-Library: HOL $(LOG)/HOL-Library.gz
 
 $(LOG)/HOL-Library.gz: $(OUT)/HOL \
   Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
   Library/Efficient_Nat.thy Library/Executable_Set.thy \
-  Library/Infinite_Set.thy \
+  Library/Infinite_Set.thy Library/Dense_Linear_Order.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/Pocklington.thy Library/Quotient.thy \
   Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy \