# HG changeset patch
# User haftmann
# Date 1245751713 -7200
# Node ID 1a92eb45060f198ce87db6217fb26d399e0d93e7
# Parent  ba52fcfaec289c661a68d4b07677b6b19b2cda04
NewNumberTheory depends on Algebra

diff -r ba52fcfaec28 -r 1a92eb45060f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jun 23 11:32:12 2009 +0200
+++ b/src/HOL/IsaMakefile	Tue Jun 23 12:08:33 2009 +0200
@@ -91,12 +91,12 @@
   $(SRC)/Tools/IsaPlanner/zipper.ML \
   $(SRC)/Tools/atomize_elim.ML \
   $(SRC)/Tools/auto_solve.ML \
-  $(SRC)/Tools/code/code_haskell.ML \
-  $(SRC)/Tools/code/code_ml.ML \
-  $(SRC)/Tools/code/code_preproc.ML \
-  $(SRC)/Tools/code/code_printer.ML \
-  $(SRC)/Tools/code/code_target.ML \
-  $(SRC)/Tools/code/code_thingol.ML \
+  $(SRC)/Tools/Code/code_haskell.ML \
+  $(SRC)/Tools/Code/code_ml.ML \
+  $(SRC)/Tools/Code/code_preproc.ML \
+  $(SRC)/Tools/Code/code_printer.ML \
+  $(SRC)/Tools/Code/code_target.ML \
+  $(SRC)/Tools/Code/code_thingol.ML \
   $(SRC)/Tools/coherent.ML \
   $(SRC)/Tools/eqsubst.ML \
   $(SRC)/Tools/induct.ML \
@@ -142,35 +142,35 @@
   Sum_Type.thy \
   Tools/arith_data.ML \
   Tools/cnf_funcs.ML \
-  Tools/datatype_package/datatype_abs_proofs.ML \
-  Tools/datatype_package/datatype_aux.ML \
-  Tools/datatype_package/datatype_case.ML \
-  Tools/datatype_package/datatype_codegen.ML \
-  Tools/datatype_package/datatype.ML \
-  Tools/datatype_package/datatype_prop.ML \
-  Tools/datatype_package/datatype_realizer.ML \
-  Tools/datatype_package/datatype_rep_proofs.ML \
+  Tools/Datatype/datatype_abs_proofs.ML \
+  Tools/Datatype/datatype_aux.ML \
+  Tools/Datatype/datatype_case.ML \
+  Tools/Datatype/datatype_codegen.ML \
+  Tools/Datatype/datatype.ML \
+  Tools/Datatype/datatype_prop.ML \
+  Tools/Datatype/datatype_realizer.ML \
+  Tools/Datatype/datatype_rep_proofs.ML \
   Tools/dseq.ML \
-  Tools/function_package/auto_term.ML \
-  Tools/function_package/context_tree.ML \
-  Tools/function_package/decompose.ML \
-  Tools/function_package/descent.ML \
-  Tools/function_package/fundef_common.ML \
-  Tools/function_package/fundef_core.ML \
-  Tools/function_package/fundef_datatype.ML \
-  Tools/function_package/fundef_lib.ML \
-  Tools/function_package/fundef.ML \
-  Tools/function_package/induction_scheme.ML \
-  Tools/function_package/inductive_wrap.ML \
-  Tools/function_package/lexicographic_order.ML \
-  Tools/function_package/measure_functions.ML \
-  Tools/function_package/mutual.ML \
-  Tools/function_package/pattern_split.ML \
-  Tools/function_package/scnp_reconstruct.ML \
-  Tools/function_package/scnp_solve.ML \
-  Tools/function_package/size.ML \
-  Tools/function_package/sum_tree.ML \
-  Tools/function_package/termination.ML \
+  Tools/Function/auto_term.ML \
+  Tools/Function/context_tree.ML \
+  Tools/Function/decompose.ML \
+  Tools/Function/descent.ML \
+  Tools/Function/fundef_common.ML \
+  Tools/Function/fundef_core.ML \
+  Tools/Function/fundef_datatype.ML \
+  Tools/Function/fundef_lib.ML \
+  Tools/Function/fundef.ML \
+  Tools/Function/induction_scheme.ML \
+  Tools/Function/inductive_wrap.ML \
+  Tools/Function/lexicographic_order.ML \
+  Tools/Function/measure_functions.ML \
+  Tools/Function/mutual.ML \
+  Tools/Function/pattern_split.ML \
+  Tools/Function/scnp_reconstruct.ML \
+  Tools/Function/scnp_solve.ML \
+  Tools/Function/size.ML \
+  Tools/Function/sum_tree.ML \
+  Tools/Function/termination.ML \
   Tools/inductive_codegen.ML \
   Tools/inductive.ML \
   Tools/inductive_realizer.ML \
@@ -429,7 +429,7 @@
 IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
   Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
   Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
-  Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
+  Import/hol4rews.ML Import/import.ML Import/ROOT.ML
 
 HOL-Import: HOL $(LOG)/HOL-Import.gz
 
@@ -494,11 +494,14 @@
 
 HOL-NewNumberTheory: HOL $(LOG)/HOL-NewNumberTheory.gz
 
-$(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL $(LOG)/HOL-Algebra.gz \
-  GCD.thy Library/Multiset.thy	\
-  NewNumberTheory/Fib.thy NewNumberTheory/Binomial.thy			\
-  NewNumberTheory/Residues.thy NewNumberTheory/UniqueFactorization.thy  \
-  NewNumberTheory/Cong.thy NewNumberTheory/MiscAlgebra.thy \
+$(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
+  Library/Multiset.thy \
+  NewNumberTheory/Binomial.thy \
+  NewNumberTheory/Cong.thy \
+  NewNumberTheory/Fib.thy \
+  NewNumberTheory/MiscAlgebra.thy \
+  NewNumberTheory/Residues.thy \
+  NewNumberTheory/UniqueFactorization.thy  \
   NewNumberTheory/ROOT.ML
 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NewNumberTheory
 
@@ -567,22 +570,46 @@
 
 HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
 
-$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML			\
-  Library/Binomial.thy Library/FuncSet.thy				\
-  Library/Multiset.thy Library/Permutation.thy Library/Primes.thy	\
-  Algebra/AbelCoset.thy Algebra/Bij.thy	Algebra/Congruence.thy		\
-  Algebra/Coset.thy Algebra/Divisibility.thy Algebra/Exponent.thy	\
-  Algebra/FiniteProduct.thy						\
-  Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy		\
-  Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy		\
-  Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy		\
-  Algebra/UnivPoly.thy Algebra/abstract/Abstract.thy			\
-  Algebra/abstract/Factor.thy Algebra/abstract/Field.thy		\
-  Algebra/abstract/Ideal2.thy Algebra/abstract/PID.thy			\
-  Algebra/abstract/Ring2.thy Algebra/abstract/RingHomo.thy		\
-  Algebra/document/root.tex Algebra/poly/LongDiv.thy			\
-  Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy			\
-  Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML
+ALGEBRA_DEPENDENCIES = $(OUT)/HOL \
+  Algebra/ROOT.ML \
+  Library/Binomial.thy \
+  Library/FuncSet.thy \
+  Library/Multiset.thy \
+  Library/Permutation.thy \
+  Library/Primes.thy \
+  Algebra/AbelCoset.thy \
+  Algebra/Bij.thy \
+  Algebra/Congruence.thy \
+  Algebra/Coset.thy \
+  Algebra/Divisibility.thy \
+  Algebra/Exponent.thy \
+  Algebra/FiniteProduct.thy \
+  Algebra/Group.thy \
+  Algebra/Ideal.thy \
+  Algebra/IntRing.thy \
+  Algebra/Lattice.thy \
+  Algebra/Module.thy \
+  Algebra/QuotRing.thy \
+  Algebra/Ring.thy \
+  Algebra/RingHom.thy \
+  Algebra/Sylow.thy \
+  Algebra/UnivPoly.thy \
+  Algebra/abstract/Abstract.thy \
+  Algebra/abstract/Factor.thy \
+  Algebra/abstract/Field.thy \
+  Algebra/abstract/Ideal2.thy \
+  Algebra/abstract/PID.thy \
+  Algebra/abstract/Ring2.thy \
+  Algebra/abstract/RingHomo.thy \
+  Algebra/document/root.tex \
+  Algebra/document/root.tex \
+  Algebra/poly/LongDiv.thy \
+  Algebra/poly/PolyHomo.thy \
+  Algebra/poly/Polynomial.thy \
+  Algebra/poly/UnivPoly2.thy \
+  Algebra/ringsimp.ML
+
+$(LOG)/HOL-Algebra.gz: $(ALGEBRA_DEPENDENCIES)
 	@cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra