# HG changeset patch
# User wenzelm
# Date 1185712190 -7200
# Node ID 936cc23a34727b9e62ebeced5c5c69074a5838e2
# Parent  74c032aea9ed073c3666eb635a34b5b433f4422b
removed obsolete Tools/res_atpset.ML;

diff -r 74c032aea9ed -r 936cc23a3472 src/HOL/IsaMakefile
--- 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	\
diff -r 74c032aea9ed -r 936cc23a3472 src/HOL/Tools/res_atpset.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;