--- a/src/HOL/IsaMakefile Thu May 31 11:00:06 2007 +0200
+++ b/src/HOL/IsaMakefile Thu May 31 12:06:31 2007 +0200
@@ -62,8 +62,7 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/HOL: $(OUT)/Pure $(SRC)/Pure/General/int.ML $(SRC)/Pure/General/rat.ML \
- $(SRC)/Provers/Arith/abel_cancel.ML \
+$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
$(SRC)/Provers/Arith/assoc_fold.ML \
$(SRC)/Provers/Arith/cancel_div_mod.ML \
$(SRC)/Provers/Arith/cancel_numeral_factor.ML \
@@ -81,40 +80,42 @@
$(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML \
$(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \
- $(SRC)/Provers/trancl.ML $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML \
- $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML \
- $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML $(SRC)/TFL/usyntax.ML \
- $(SRC)/TFL/utils.ML ATP_Linkup.thy Accessible_Part.thy \
- Code_Generator.thy Datatype.thy Divides.thy Equiv_Relations.thy \
- Extraction.thy Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy \
- HOL.thy Hilbert_Choice.thy Inductive.thy Integ/IntArith.thy \
- Integ/IntDef.thy Integ/IntDiv.thy Integ/NatBin.thy \
- Integ/NatSimprocs.thy Integ/Numeral.thy Integ/Presburger.thy \
- Integ/cooper_dec.ML Integ/cooper_proof.ML Integ/int_arith1.ML \
- Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML Integ/presburger.ML \
- Integ/qelim.ML Integ/reflected_cooper.ML Integ/reflected_presburger.ML \
- Lattices.thy List.thy Main.thy Map.thy Nat.ML Nat.thy \
- OrderedGroup.thy Orderings.thy Power.thy Predicate.thy PreList.thy \
+ $(SRC)/Provers/trancl.ML $(SRC)/Pure/General/int.ML \
+ $(SRC)/Pure/General/rat.ML $(SRC)/TFL/casesplit.ML \
+ $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
+ $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
+ $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML ATP_Linkup.thy \
+ Accessible_Part.thy Code_Generator.thy Datatype.thy Divides.thy \
+ Equiv_Relations.thy Extraction.thy Finite_Set.thy FixedPoint.thy \
+ Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy Inductive.thy \
+ Integ/IntArith.thy Integ/IntDef.thy Integ/IntDiv.thy Integ/NatBin.thy \
+ Integ/NatSimprocs.thy Integ/Numeral.thy Integ/int_arith1.ML \
+ Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML Lattices.thy \
+ List.thy Main.thy Map.thy Nat.ML Nat.thy OrderedGroup.thy \
+ Orderings.thy Power.thy PreList.thy Predicate.thy Presburger.thy \
Product_Type.thy ROOT.ML Recdef.thy Record.thy Refute.thy Relation.thy \
Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy \
- Sum_Type.thy Tools/res_reconstruct.ML Tools/ATP/reduce_axiomsN.ML \
- Tools/ATP/watcher.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML \
- Tools/datatype_aux.ML Tools/datatype_case.ML Tools/datatype_codegen.ML \
+ Sum_Type.thy Tools/ATP/reduce_axiomsN.ML Tools/ATP/watcher.ML \
+ Tools/Presburger/cooper_dec.ML Tools/Presburger/cooper_proof.ML \
+ Tools/Presburger/presburger.ML Tools/Presburger/qelim.ML \
+ Tools/Presburger/reflected_cooper.ML \
+ Tools/Presburger/reflected_presburger.ML Tools/cnf_funcs.ML \
+ Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
+ Tools/datatype_case.ML Tools/datatype_codegen.ML \
Tools/datatype_hooks.ML Tools/datatype_package.ML \
Tools/datatype_prop.ML Tools/datatype_realizer.ML \
Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML \
Tools/function_package/context_tree.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_package.ML \
- Tools/function_package/fundef_core.ML \
Tools/function_package/inductive_wrap.ML \
Tools/function_package/lexicographic_order.ML \
Tools/function_package/mutual.ML \
Tools/function_package/pattern_split.ML \
- Tools/function_package/sum_tools.ML \
- Tools/inductive_codegen.ML \
+ Tools/function_package/sum_tools.ML Tools/inductive_codegen.ML \
Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML \
Tools/numeral_syntax.ML Tools/old_inductive_package.ML \
Tools/polyhash.ML Tools/primrec_package.ML Tools/prop_logic.ML \
@@ -122,8 +123,9 @@
Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML \
Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML \
Tools/res_atpset.ML Tools/res_axioms.ML Tools/res_clause.ML \
- Tools/res_hol_clause.ML Tools/rewrite_hol_proof.ML Tools/sat_funcs.ML \
- Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML \
+ Tools/res_hol_clause.ML Tools/res_reconstruct.ML \
+ Tools/rewrite_hol_proof.ML Tools/sat_funcs.ML Tools/sat_solver.ML \
+ Tools/specification_package.ML Tools/split_rule.ML \
Tools/string_syntax.ML Tools/typecopy_package.ML \
Tools/typedef_codegen.ML Tools/typedef_package.ML \
Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy \