src/HOL/Tools/res_atpset.ML
author paulson
Fri Nov 24 16:38:42 2006 +0100 (2006-11-24)
changeset 21513 9e9fff87dc6c
parent 21506 b2a673894ce5
child 22846 fb79144af9a3
permissions -rw-r--r--
Conversion of "equal" to "=" for TSTP format; big tidy-up
     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   val name = "HOL/atpset";
    22   type T = thm list;
    23   val empty = [];
    24   val extend = I;
    25   fun merge _ = Drule.merge_rules;
    26   fun print context rules =
    27     Pretty.writeln (Pretty.big_list "ATP rules:"
    28       (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
    29 );
    30 
    31 val print_atpset = Data.print o Context.Proof;
    32 val get_atpset = Data.get o Context.Proof;
    33 
    34 val atp_add = Thm.declaration_attribute (Data.map o Drule.add_rule);
    35 val atp_del = Thm.declaration_attribute (Data.map o Drule.del_rule);
    36 
    37 val setup =
    38   Data.init #>
    39   Attrib.add_attributes [("atp", Attrib.add_del_args atp_add atp_del, "declaration of ATP rules")];
    40 
    41 end;