89 $(SRC)/Tools/IsaPlanner/rw_inst.ML \ |
89 $(SRC)/Tools/IsaPlanner/rw_inst.ML \ |
90 $(SRC)/Tools/IsaPlanner/rw_tools.ML \ |
90 $(SRC)/Tools/IsaPlanner/rw_tools.ML \ |
91 $(SRC)/Tools/IsaPlanner/zipper.ML \ |
91 $(SRC)/Tools/IsaPlanner/zipper.ML \ |
92 $(SRC)/Tools/atomize_elim.ML \ |
92 $(SRC)/Tools/atomize_elim.ML \ |
93 $(SRC)/Tools/auto_solve.ML \ |
93 $(SRC)/Tools/auto_solve.ML \ |
94 $(SRC)/Tools/code/code_haskell.ML \ |
94 $(SRC)/Tools/Code/code_haskell.ML \ |
95 $(SRC)/Tools/code/code_ml.ML \ |
95 $(SRC)/Tools/Code/code_ml.ML \ |
96 $(SRC)/Tools/code/code_preproc.ML \ |
96 $(SRC)/Tools/Code/code_preproc.ML \ |
97 $(SRC)/Tools/code/code_printer.ML \ |
97 $(SRC)/Tools/Code/code_printer.ML \ |
98 $(SRC)/Tools/code/code_target.ML \ |
98 $(SRC)/Tools/Code/code_target.ML \ |
99 $(SRC)/Tools/code/code_thingol.ML \ |
99 $(SRC)/Tools/Code/code_thingol.ML \ |
100 $(SRC)/Tools/coherent.ML \ |
100 $(SRC)/Tools/coherent.ML \ |
101 $(SRC)/Tools/eqsubst.ML \ |
101 $(SRC)/Tools/eqsubst.ML \ |
102 $(SRC)/Tools/induct.ML \ |
102 $(SRC)/Tools/induct.ML \ |
103 $(SRC)/Tools/intuitionistic.ML \ |
103 $(SRC)/Tools/intuitionistic.ML \ |
104 $(SRC)/Tools/induct_tacs.ML \ |
104 $(SRC)/Tools/induct_tacs.ML \ |
140 SAT.thy \ |
140 SAT.thy \ |
141 Set.thy \ |
141 Set.thy \ |
142 Sum_Type.thy \ |
142 Sum_Type.thy \ |
143 Tools/arith_data.ML \ |
143 Tools/arith_data.ML \ |
144 Tools/cnf_funcs.ML \ |
144 Tools/cnf_funcs.ML \ |
145 Tools/datatype_package/datatype_abs_proofs.ML \ |
145 Tools/Datatype/datatype_abs_proofs.ML \ |
146 Tools/datatype_package/datatype_aux.ML \ |
146 Tools/Datatype/datatype_aux.ML \ |
147 Tools/datatype_package/datatype_case.ML \ |
147 Tools/Datatype/datatype_case.ML \ |
148 Tools/datatype_package/datatype_codegen.ML \ |
148 Tools/Datatype/datatype_codegen.ML \ |
149 Tools/datatype_package/datatype.ML \ |
149 Tools/Datatype/datatype.ML \ |
150 Tools/datatype_package/datatype_prop.ML \ |
150 Tools/Datatype/datatype_prop.ML \ |
151 Tools/datatype_package/datatype_realizer.ML \ |
151 Tools/Datatype/datatype_realizer.ML \ |
152 Tools/datatype_package/datatype_rep_proofs.ML \ |
152 Tools/Datatype/datatype_rep_proofs.ML \ |
153 Tools/dseq.ML \ |
153 Tools/dseq.ML \ |
154 Tools/function_package/auto_term.ML \ |
154 Tools/Function/auto_term.ML \ |
155 Tools/function_package/context_tree.ML \ |
155 Tools/Function/context_tree.ML \ |
156 Tools/function_package/decompose.ML \ |
156 Tools/Function/decompose.ML \ |
157 Tools/function_package/descent.ML \ |
157 Tools/Function/descent.ML \ |
158 Tools/function_package/fundef_common.ML \ |
158 Tools/Function/fundef_common.ML \ |
159 Tools/function_package/fundef_core.ML \ |
159 Tools/Function/fundef_core.ML \ |
160 Tools/function_package/fundef_datatype.ML \ |
160 Tools/Function/fundef_datatype.ML \ |
161 Tools/function_package/fundef_lib.ML \ |
161 Tools/Function/fundef_lib.ML \ |
162 Tools/function_package/fundef.ML \ |
162 Tools/Function/fundef.ML \ |
163 Tools/function_package/induction_scheme.ML \ |
163 Tools/Function/induction_scheme.ML \ |
164 Tools/function_package/inductive_wrap.ML \ |
164 Tools/Function/inductive_wrap.ML \ |
165 Tools/function_package/lexicographic_order.ML \ |
165 Tools/Function/lexicographic_order.ML \ |
166 Tools/function_package/measure_functions.ML \ |
166 Tools/Function/measure_functions.ML \ |
167 Tools/function_package/mutual.ML \ |
167 Tools/Function/mutual.ML \ |
168 Tools/function_package/pattern_split.ML \ |
168 Tools/Function/pattern_split.ML \ |
169 Tools/function_package/scnp_reconstruct.ML \ |
169 Tools/Function/scnp_reconstruct.ML \ |
170 Tools/function_package/scnp_solve.ML \ |
170 Tools/Function/scnp_solve.ML \ |
171 Tools/function_package/size.ML \ |
171 Tools/Function/size.ML \ |
172 Tools/function_package/sum_tree.ML \ |
172 Tools/Function/sum_tree.ML \ |
173 Tools/function_package/termination.ML \ |
173 Tools/Function/termination.ML \ |
174 Tools/inductive_codegen.ML \ |
174 Tools/inductive_codegen.ML \ |
175 Tools/inductive.ML \ |
175 Tools/inductive.ML \ |
176 Tools/inductive_realizer.ML \ |
176 Tools/inductive_realizer.ML \ |
177 Tools/inductive_set.ML \ |
177 Tools/inductive_set.ML \ |
178 Tools/lin_arith.ML \ |
178 Tools/lin_arith.ML \ |
427 Import/hol4rews.ML Import/import.ML Import/ROOT.ML |
427 Import/hol4rews.ML Import/import.ML Import/ROOT.ML |
428 |
428 |
429 IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \ |
429 IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \ |
430 Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ |
430 Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ |
431 Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \ |
431 Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \ |
432 Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML |
432 Import/hol4rews.ML Import/import.ML Import/ROOT.ML |
433 |
433 |
434 HOL-Import: HOL $(LOG)/HOL-Import.gz |
434 HOL-Import: HOL $(LOG)/HOL-Import.gz |
435 |
435 |
436 $(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES) |
436 $(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES) |
437 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Import |
437 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Import |
492 |
492 |
493 ## HOL-NewNumberTheory |
493 ## HOL-NewNumberTheory |
494 |
494 |
495 HOL-NewNumberTheory: HOL $(LOG)/HOL-NewNumberTheory.gz |
495 HOL-NewNumberTheory: HOL $(LOG)/HOL-NewNumberTheory.gz |
496 |
496 |
497 $(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL $(LOG)/HOL-Algebra.gz \ |
497 $(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \ |
498 GCD.thy Library/Multiset.thy \ |
498 Library/Multiset.thy \ |
499 NewNumberTheory/Fib.thy NewNumberTheory/Binomial.thy \ |
499 NewNumberTheory/Binomial.thy \ |
500 NewNumberTheory/Residues.thy NewNumberTheory/UniqueFactorization.thy \ |
500 NewNumberTheory/Cong.thy \ |
501 NewNumberTheory/Cong.thy NewNumberTheory/MiscAlgebra.thy \ |
501 NewNumberTheory/Fib.thy \ |
|
502 NewNumberTheory/MiscAlgebra.thy \ |
|
503 NewNumberTheory/Residues.thy \ |
|
504 NewNumberTheory/UniqueFactorization.thy \ |
502 NewNumberTheory/ROOT.ML |
505 NewNumberTheory/ROOT.ML |
503 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NewNumberTheory |
506 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NewNumberTheory |
504 |
507 |
505 |
508 |
506 ## HOL-NumberTheory |
509 ## HOL-NumberTheory |
565 |
568 |
566 ## HOL-Algebra |
569 ## HOL-Algebra |
567 |
570 |
568 HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz |
571 HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz |
569 |
572 |
570 $(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \ |
573 ALGEBRA_DEPENDENCIES = $(OUT)/HOL \ |
571 Library/Binomial.thy Library/FuncSet.thy \ |
574 Algebra/ROOT.ML \ |
572 Library/Multiset.thy Library/Permutation.thy Library/Primes.thy \ |
575 Library/Binomial.thy \ |
573 Algebra/AbelCoset.thy Algebra/Bij.thy Algebra/Congruence.thy \ |
576 Library/FuncSet.thy \ |
574 Algebra/Coset.thy Algebra/Divisibility.thy Algebra/Exponent.thy \ |
577 Library/Multiset.thy \ |
575 Algebra/FiniteProduct.thy \ |
578 Library/Permutation.thy \ |
576 Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy \ |
579 Library/Primes.thy \ |
577 Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy \ |
580 Algebra/AbelCoset.thy \ |
578 Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy \ |
581 Algebra/Bij.thy \ |
579 Algebra/UnivPoly.thy Algebra/abstract/Abstract.thy \ |
582 Algebra/Congruence.thy \ |
580 Algebra/abstract/Factor.thy Algebra/abstract/Field.thy \ |
583 Algebra/Coset.thy \ |
581 Algebra/abstract/Ideal2.thy Algebra/abstract/PID.thy \ |
584 Algebra/Divisibility.thy \ |
582 Algebra/abstract/Ring2.thy Algebra/abstract/RingHomo.thy \ |
585 Algebra/Exponent.thy \ |
583 Algebra/document/root.tex Algebra/poly/LongDiv.thy \ |
586 Algebra/FiniteProduct.thy \ |
584 Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy \ |
587 Algebra/Group.thy \ |
585 Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML |
588 Algebra/Ideal.thy \ |
|
589 Algebra/IntRing.thy \ |
|
590 Algebra/Lattice.thy \ |
|
591 Algebra/Module.thy \ |
|
592 Algebra/QuotRing.thy \ |
|
593 Algebra/Ring.thy \ |
|
594 Algebra/RingHom.thy \ |
|
595 Algebra/Sylow.thy \ |
|
596 Algebra/UnivPoly.thy \ |
|
597 Algebra/abstract/Abstract.thy \ |
|
598 Algebra/abstract/Factor.thy \ |
|
599 Algebra/abstract/Field.thy \ |
|
600 Algebra/abstract/Ideal2.thy \ |
|
601 Algebra/abstract/PID.thy \ |
|
602 Algebra/abstract/Ring2.thy \ |
|
603 Algebra/abstract/RingHomo.thy \ |
|
604 Algebra/document/root.tex \ |
|
605 Algebra/document/root.tex \ |
|
606 Algebra/poly/LongDiv.thy \ |
|
607 Algebra/poly/PolyHomo.thy \ |
|
608 Algebra/poly/Polynomial.thy \ |
|
609 Algebra/poly/UnivPoly2.thy \ |
|
610 Algebra/ringsimp.ML |
|
611 |
|
612 $(LOG)/HOL-Algebra.gz: $(ALGEBRA_DEPENDENCIES) |
586 @cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra |
613 @cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra |
587 |
614 |
588 |
615 |
589 ## HOL-Auth |
616 ## HOL-Auth |
590 |
617 |