src/HOL/Tools/res_atpset.ML

Hyperreal/FrechetDeriv.thy

(*  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
(
  val name = "HOL/atpset";
  type T = thm list;
  val empty = [];
  val extend = I;
  fun merge _ = Drule.merge_rules;
  fun print context rules =
    Pretty.writeln (Pretty.big_list "ATP rules:"
      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
);

val print_atpset = Data.print o Context.Proof;
val get_atpset = Data.get o Context.Proof;

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 =
  Data.init #>
  Attrib.add_attributes [("atp", Attrib.add_del_args atp_add atp_del, "declaration of ATP rules")];

end;