HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated
authorchaieb
Wed, 27 Feb 2008 14:39:49 +0100
changeset 26155 7c265e3da23c
parent 26154 894f3860ebfd
child 26156 420c1947511c
HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated
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 \