# HG changeset patch
# User chaieb
# Date 1204119589 -3600
# Node ID 7c265e3da23cbc2809e707cdd5fb81647187d154
# Parent  894f3860ebfdc6df206ea10f357df0bbf7bc3e5a
HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated

diff -r 894f3860ebfd -r 7c265e3da23c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Feb 27 14:39:48 2008 +0100
+++ b/src/HOL/IsaMakefile	Wed Feb 27 14:39:49 2008 +0100
@@ -93,7 +93,7 @@
   $(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	\
@@ -215,7 +215,7 @@
 $(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 \