src/HOL/Tools/res_atpset.ML

some tests for arith added

(*  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;