--- a/src/HOL/IsaMakefile Sun Dec 10 17:37:55 2006 +0100
+++ b/src/HOL/IsaMakefile Sun Dec 10 19:37:25 2006 +0100
@@ -70,71 +70,65 @@
$(SRC)/Provers/Arith/cancel_sums.ML \
$(SRC)/Provers/Arith/combine_numerals.ML \
$(SRC)/Provers/Arith/extract_common_term.ML \
- $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
+ $(SRC)/Provers/Arith/fast_lin_arith.ML \
+ $(SRC)/Provers/IsaPlanner/isand.ML \
+ $(SRC)/Provers/IsaPlanner/rw_inst.ML \
+ $(SRC)/Provers/IsaPlanner/rw_tools.ML \
+ $(SRC)/Provers/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
- $(SRC)/Provers/IsaPlanner/zipper.ML \
- $(SRC)/Provers/IsaPlanner/isand.ML \
- $(SRC)/Provers/IsaPlanner/rw_tools.ML \
- $(SRC)/Provers/IsaPlanner/rw_inst.ML \
$(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \
$(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 \
- Tools/res_atpset.ML \
- Code_Generator.thy Datatype.thy Divides.thy \
- Equiv_Relations.thy Extraction.thy Finite_Set.thy \
- FixedPoint.thy Fun.thy HOL.ML 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/reflected_presburger.ML \
- Integ/reflected_cooper.ML Integ/int_arith1.ML Integ/int_factor_simprocs.ML \
- Integ/nat_simprocs.ML Integ/presburger.ML Integ/qelim.ML LOrder.thy \
- Lattices.thy List.thy Main.thy Map.thy Nat.thy Nat.ML OrderedGroup.ML \
- OrderedGroup.thy Orderings.thy Power.thy PreList.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/ATP/AtpCommunication.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_codegen.ML Tools/datatype_hooks.ML Tools/datatype_package.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.ML \
+ 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 \
+ LOrder.thy Lattices.thy List.thy Main.thy Map.thy Nat.ML Nat.thy \
+ OrderedGroup.ML OrderedGroup.thy Orderings.thy Power.thy PreList.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/ATP/AtpCommunication.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_codegen.ML \
+ Tools/datatype_hooks.ML Tools/datatype_package.ML \
Tools/datatype_prop.ML Tools/datatype_realizer.ML \
- Tools/datatype_rep_proofs.ML Tools/inductive_codegen.ML \
- Tools/inductive_package.ML Tools/old_inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML \
- Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/prop_logic.ML \
- Tools/polyhash.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_datatype.ML \
+ Tools/function_package/fundef_lib.ML \
+ Tools/function_package/fundef_package.ML \
+ Tools/function_package/fundef_prep.ML \
+ Tools/function_package/fundef_proof.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/function_package/termination.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 \
Tools/recdef_package.ML Tools/recfun_codegen.ML \
- Tools/record_package.ML Tools/refute.ML \
- Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML \
- Tools/res_clause.ML Tools/rewrite_hol_proof.ML \
- Tools/sat_funcs.ML \
+ 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/typecopy_package.ML \
- Tools/typedef_package.ML Tools/typedef_codegen.ML \
- Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy \
- Wellfounded_Relations.thy arith_data.ML \
- document/root.tex hologic.ML simpdata.ML ATP_Linkup.thy \
- Tools/res_atp_provers.ML Tools/res_atp_methods.ML \
- Tools/res_hol_clause.ML \
- Tools/function_package/sum_tools.ML \
- Tools/function_package/fundef_common.ML \
- Tools/function_package/fundef_lib.ML \
- Tools/function_package/inductive_wrap.ML \
- Tools/function_package/context_tree.ML \
- Tools/function_package/fundef_prep.ML \
- Tools/function_package/fundef_proof.ML \
- Tools/function_package/termination.ML \
- Tools/function_package/pattern_split.ML \
- Tools/function_package/mutual.ML \
- Tools/function_package/fundef_package.ML \
- Tools/function_package/auto_term.ML \
- Tools/function_package/lexicographic_order.ML \
- Tools/function_package/fundef_datatype.ML \
- FunDef.thy Accessible_Part.thy
+ Tools/string_syntax.ML Tools/typecopy_package.ML \
+ Tools/typedef_codegen.ML Tools/typedef_package.ML \
+ Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy \
+ Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML \
+ simpdata.ML
@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL