--- a/src/HOL/IsaMakefile Sun Jul 29 14:29:49 2007 +0200
+++ b/src/HOL/IsaMakefile Sun Jul 29 14:29:50 2007 +0200
@@ -124,11 +124,10 @@
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 \
+ 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 \
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 \
--- a/src/HOL/Tools/res_atpset.ML Sun Jul 29 14:29:49 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(* ID: $Id$
- Author: Jia Meng, NICTA
-
-ATP rules.
-*)
-
-signature RES_ATPSET =
-sig
- val print_atpset: Proof.context -> unit
- val get_atpset: Proof.context -> thm list
- val atp_add: attribute
- val atp_del: attribute
- val setup: theory -> theory
-end;
-
-structure ResAtpset: RES_ATPSET =
-struct
-
-structure Data = GenericDataFun
-(
- type T = thm list;
- val empty = [];
- val extend = I;
- fun merge _ = Drule.merge_rules;
-);
-
-val get_atpset = Data.get o Context.Proof;
-
-fun print_atpset ctxt =
- Pretty.writeln (Pretty.big_list "ATP rules:"
- (map (ProofContext.pretty_thm ctxt) (get_atpset ctxt)));
-
-val atp_add = Thm.declaration_attribute (Data.map o Drule.add_rule);
-val atp_del = Thm.declaration_attribute (Data.map o Drule.del_rule);
-
-val setup =
- Attrib.add_attributes [("atp", Attrib.add_del_args atp_add atp_del, "declaration of ATP rules")];
-
-end;