# HG changeset patch # User wenzelm # Date 1182374357 -7200 # Node ID 6908c13215d1e5a9469cc2557adb84e73d9657a6 # Parent 6d4703843f93555c81e4e2d07795435b0137683a added Tools/metis_tools.ML; diff -r 6d4703843f93 -r 6908c13215d1 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jun 20 23:19:16 2007 +0200 +++ b/src/HOL/IsaMakefile Wed Jun 20 23:19:17 2007 +0200 @@ -118,13 +118,13 @@ Tools/function_package/pattern_split.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 \ - 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_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/res_reconstruct.ML \ + Tools/metis_tools.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_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/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 \