src/HOL/Tools/res_atpset.ML
author paulson
Tue May 22 17:56:06 2007 +0200 (2007-05-22)
changeset 23075 69e30a7e8880
parent 22846 fb79144af9a3
permissions -rw-r--r--
Some hacks for SPASS format
     1 (*  ID:         $Id$
     2     Author:     Jia Meng, NICTA
     3 
     4 ATP rules.
     5 *)
     6 
     7 signature RES_ATPSET =
     8 sig
     9   val print_atpset: Proof.context -> unit
    10   val get_atpset: Proof.context -> thm list
    11   val atp_add: attribute
    12   val atp_del: attribute
    13   val setup: theory -> theory
    14 end;
    15 
    16 structure ResAtpset: RES_ATPSET =
    17 struct
    18 
    19 structure Data = GenericDataFun
    20 (
    21   type T = thm list;
    22   val empty = [];
    23   val extend = I;
    24   fun merge _ = Drule.merge_rules;
    25 );
    26 
    27 val get_atpset = Data.get o Context.Proof;
    28 
    29 fun print_atpset ctxt =
    30   Pretty.writeln (Pretty.big_list "ATP rules:"
    31     (map (ProofContext.pretty_thm ctxt) (get_atpset ctxt)));
    32 
    33 val atp_add = Thm.declaration_attribute (Data.map o Drule.add_rule);
    34 val atp_del = Thm.declaration_attribute (Data.map o Drule.del_rule);
    35 
    36 val setup =
    37   Attrib.add_attributes [("atp", Attrib.add_del_args atp_add atp_del, "declaration of ATP rules")];
    38 
    39 end;