NewNumberTheory depends on Algebra
authorhaftmann
Tue Jun 23 12:08:33 2009 +0200 (2009-06-23)
changeset 317711a92eb45060f
parent 31770 ba52fcfaec28
child 31772 a946fe9a0476
NewNumberTheory depends on Algebra
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Tue Jun 23 11:32:12 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jun 23 12:08:33 2009 +0200
     1.3 @@ -91,12 +91,12 @@
     1.4    $(SRC)/Tools/IsaPlanner/zipper.ML \
     1.5    $(SRC)/Tools/atomize_elim.ML \
     1.6    $(SRC)/Tools/auto_solve.ML \
     1.7 -  $(SRC)/Tools/code/code_haskell.ML \
     1.8 -  $(SRC)/Tools/code/code_ml.ML \
     1.9 -  $(SRC)/Tools/code/code_preproc.ML \
    1.10 -  $(SRC)/Tools/code/code_printer.ML \
    1.11 -  $(SRC)/Tools/code/code_target.ML \
    1.12 -  $(SRC)/Tools/code/code_thingol.ML \
    1.13 +  $(SRC)/Tools/Code/code_haskell.ML \
    1.14 +  $(SRC)/Tools/Code/code_ml.ML \
    1.15 +  $(SRC)/Tools/Code/code_preproc.ML \
    1.16 +  $(SRC)/Tools/Code/code_printer.ML \
    1.17 +  $(SRC)/Tools/Code/code_target.ML \
    1.18 +  $(SRC)/Tools/Code/code_thingol.ML \
    1.19    $(SRC)/Tools/coherent.ML \
    1.20    $(SRC)/Tools/eqsubst.ML \
    1.21    $(SRC)/Tools/induct.ML \
    1.22 @@ -142,35 +142,35 @@
    1.23    Sum_Type.thy \
    1.24    Tools/arith_data.ML \
    1.25    Tools/cnf_funcs.ML \
    1.26 -  Tools/datatype_package/datatype_abs_proofs.ML \
    1.27 -  Tools/datatype_package/datatype_aux.ML \
    1.28 -  Tools/datatype_package/datatype_case.ML \
    1.29 -  Tools/datatype_package/datatype_codegen.ML \
    1.30 -  Tools/datatype_package/datatype.ML \
    1.31 -  Tools/datatype_package/datatype_prop.ML \
    1.32 -  Tools/datatype_package/datatype_realizer.ML \
    1.33 -  Tools/datatype_package/datatype_rep_proofs.ML \
    1.34 +  Tools/Datatype/datatype_abs_proofs.ML \
    1.35 +  Tools/Datatype/datatype_aux.ML \
    1.36 +  Tools/Datatype/datatype_case.ML \
    1.37 +  Tools/Datatype/datatype_codegen.ML \
    1.38 +  Tools/Datatype/datatype.ML \
    1.39 +  Tools/Datatype/datatype_prop.ML \
    1.40 +  Tools/Datatype/datatype_realizer.ML \
    1.41 +  Tools/Datatype/datatype_rep_proofs.ML \
    1.42    Tools/dseq.ML \
    1.43 -  Tools/function_package/auto_term.ML \
    1.44 -  Tools/function_package/context_tree.ML \
    1.45 -  Tools/function_package/decompose.ML \
    1.46 -  Tools/function_package/descent.ML \
    1.47 -  Tools/function_package/fundef_common.ML \
    1.48 -  Tools/function_package/fundef_core.ML \
    1.49 -  Tools/function_package/fundef_datatype.ML \
    1.50 -  Tools/function_package/fundef_lib.ML \
    1.51 -  Tools/function_package/fundef.ML \
    1.52 -  Tools/function_package/induction_scheme.ML \
    1.53 -  Tools/function_package/inductive_wrap.ML \
    1.54 -  Tools/function_package/lexicographic_order.ML \
    1.55 -  Tools/function_package/measure_functions.ML \
    1.56 -  Tools/function_package/mutual.ML \
    1.57 -  Tools/function_package/pattern_split.ML \
    1.58 -  Tools/function_package/scnp_reconstruct.ML \
    1.59 -  Tools/function_package/scnp_solve.ML \
    1.60 -  Tools/function_package/size.ML \
    1.61 -  Tools/function_package/sum_tree.ML \
    1.62 -  Tools/function_package/termination.ML \
    1.63 +  Tools/Function/auto_term.ML \
    1.64 +  Tools/Function/context_tree.ML \
    1.65 +  Tools/Function/decompose.ML \
    1.66 +  Tools/Function/descent.ML \
    1.67 +  Tools/Function/fundef_common.ML \
    1.68 +  Tools/Function/fundef_core.ML \
    1.69 +  Tools/Function/fundef_datatype.ML \
    1.70 +  Tools/Function/fundef_lib.ML \
    1.71 +  Tools/Function/fundef.ML \
    1.72 +  Tools/Function/induction_scheme.ML \
    1.73 +  Tools/Function/inductive_wrap.ML \
    1.74 +  Tools/Function/lexicographic_order.ML \
    1.75 +  Tools/Function/measure_functions.ML \
    1.76 +  Tools/Function/mutual.ML \
    1.77 +  Tools/Function/pattern_split.ML \
    1.78 +  Tools/Function/scnp_reconstruct.ML \
    1.79 +  Tools/Function/scnp_solve.ML \
    1.80 +  Tools/Function/size.ML \
    1.81 +  Tools/Function/sum_tree.ML \
    1.82 +  Tools/Function/termination.ML \
    1.83    Tools/inductive_codegen.ML \
    1.84    Tools/inductive.ML \
    1.85    Tools/inductive_realizer.ML \
    1.86 @@ -429,7 +429,7 @@
    1.87  IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
    1.88    Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
    1.89    Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
    1.90 -  Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
    1.91 +  Import/hol4rews.ML Import/import.ML Import/ROOT.ML
    1.92  
    1.93  HOL-Import: HOL $(LOG)/HOL-Import.gz
    1.94  
    1.95 @@ -494,11 +494,14 @@
    1.96  
    1.97  HOL-NewNumberTheory: HOL $(LOG)/HOL-NewNumberTheory.gz
    1.98  
    1.99 -$(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL $(LOG)/HOL-Algebra.gz \
   1.100 -  GCD.thy Library/Multiset.thy	\
   1.101 -  NewNumberTheory/Fib.thy NewNumberTheory/Binomial.thy			\
   1.102 -  NewNumberTheory/Residues.thy NewNumberTheory/UniqueFactorization.thy  \
   1.103 -  NewNumberTheory/Cong.thy NewNumberTheory/MiscAlgebra.thy \
   1.104 +$(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
   1.105 +  Library/Multiset.thy \
   1.106 +  NewNumberTheory/Binomial.thy \
   1.107 +  NewNumberTheory/Cong.thy \
   1.108 +  NewNumberTheory/Fib.thy \
   1.109 +  NewNumberTheory/MiscAlgebra.thy \
   1.110 +  NewNumberTheory/Residues.thy \
   1.111 +  NewNumberTheory/UniqueFactorization.thy  \
   1.112    NewNumberTheory/ROOT.ML
   1.113  	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NewNumberTheory
   1.114  
   1.115 @@ -567,22 +570,46 @@
   1.116  
   1.117  HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
   1.118  
   1.119 -$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML			\
   1.120 -  Library/Binomial.thy Library/FuncSet.thy				\
   1.121 -  Library/Multiset.thy Library/Permutation.thy Library/Primes.thy	\
   1.122 -  Algebra/AbelCoset.thy Algebra/Bij.thy	Algebra/Congruence.thy		\
   1.123 -  Algebra/Coset.thy Algebra/Divisibility.thy Algebra/Exponent.thy	\
   1.124 -  Algebra/FiniteProduct.thy						\
   1.125 -  Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy		\
   1.126 -  Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy		\
   1.127 -  Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy		\
   1.128 -  Algebra/UnivPoly.thy Algebra/abstract/Abstract.thy			\
   1.129 -  Algebra/abstract/Factor.thy Algebra/abstract/Field.thy		\
   1.130 -  Algebra/abstract/Ideal2.thy Algebra/abstract/PID.thy			\
   1.131 -  Algebra/abstract/Ring2.thy Algebra/abstract/RingHomo.thy		\
   1.132 -  Algebra/document/root.tex Algebra/poly/LongDiv.thy			\
   1.133 -  Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy			\
   1.134 -  Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML
   1.135 +ALGEBRA_DEPENDENCIES = $(OUT)/HOL \
   1.136 +  Algebra/ROOT.ML \
   1.137 +  Library/Binomial.thy \
   1.138 +  Library/FuncSet.thy \
   1.139 +  Library/Multiset.thy \
   1.140 +  Library/Permutation.thy \
   1.141 +  Library/Primes.thy \
   1.142 +  Algebra/AbelCoset.thy \
   1.143 +  Algebra/Bij.thy \
   1.144 +  Algebra/Congruence.thy \
   1.145 +  Algebra/Coset.thy \
   1.146 +  Algebra/Divisibility.thy \
   1.147 +  Algebra/Exponent.thy \
   1.148 +  Algebra/FiniteProduct.thy \
   1.149 +  Algebra/Group.thy \
   1.150 +  Algebra/Ideal.thy \
   1.151 +  Algebra/IntRing.thy \
   1.152 +  Algebra/Lattice.thy \
   1.153 +  Algebra/Module.thy \
   1.154 +  Algebra/QuotRing.thy \
   1.155 +  Algebra/Ring.thy \
   1.156 +  Algebra/RingHom.thy \
   1.157 +  Algebra/Sylow.thy \
   1.158 +  Algebra/UnivPoly.thy \
   1.159 +  Algebra/abstract/Abstract.thy \
   1.160 +  Algebra/abstract/Factor.thy \
   1.161 +  Algebra/abstract/Field.thy \
   1.162 +  Algebra/abstract/Ideal2.thy \
   1.163 +  Algebra/abstract/PID.thy \
   1.164 +  Algebra/abstract/Ring2.thy \
   1.165 +  Algebra/abstract/RingHomo.thy \
   1.166 +  Algebra/document/root.tex \
   1.167 +  Algebra/document/root.tex \
   1.168 +  Algebra/poly/LongDiv.thy \
   1.169 +  Algebra/poly/PolyHomo.thy \
   1.170 +  Algebra/poly/Polynomial.thy \
   1.171 +  Algebra/poly/UnivPoly2.thy \
   1.172 +  Algebra/ringsimp.ML
   1.173 +
   1.174 +$(LOG)/HOL-Algebra.gz: $(ALGEBRA_DEPENDENCIES)
   1.175  	@cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
   1.176  
   1.177