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
mengj@19159
     1
(*  ID:         $Id$
wenzelm@20773
     2
    Author:     Jia Meng, NICTA
mengj@19159
     3
wenzelm@20773
     4
ATP rules.
mengj@19159
     5
*)
mengj@19159
     6
mengj@19170
     7
signature RES_ATPSET =
mengj@19170
     8
sig
wenzelm@21506
     9
  val print_atpset: Proof.context -> unit
wenzelm@21506
    10
  val get_atpset: Proof.context -> thm list
wenzelm@20773
    11
  val atp_add: attribute
wenzelm@20773
    12
  val atp_del: attribute
wenzelm@20773
    13
  val setup: theory -> theory
mengj@19170
    14
end;
mengj@19170
    15
wenzelm@20773
    16
structure ResAtpset: RES_ATPSET =
mengj@19159
    17
struct
mengj@19159
    18
wenzelm@20773
    19
structure Data = GenericDataFun
wenzelm@20773
    20
(
wenzelm@20773
    21
  val name = "HOL/atpset";
wenzelm@20773
    22
  type T = thm list;
wenzelm@20773
    23
  val empty = [];
wenzelm@20773
    24
  val extend = I;
wenzelm@20773
    25
  fun merge _ = Drule.merge_rules;
wenzelm@20773
    26
  fun print context rules =
wenzelm@20773
    27
    Pretty.writeln (Pretty.big_list "ATP rules:"
wenzelm@20773
    28
      (map (ProofContext.pretty_thm (Context.proof_of context)) rules));
wenzelm@20773
    29
);
mengj@19159
    30
wenzelm@21506
    31
val print_atpset = Data.print o Context.Proof;
wenzelm@21506
    32
val get_atpset = Data.get o Context.Proof;
mengj@19159
    33
wenzelm@20773
    34
val atp_add = Thm.declaration_attribute (Data.map o Drule.add_rule);
wenzelm@20773
    35
val atp_del = Thm.declaration_attribute (Data.map o Drule.del_rule);
mengj@19159
    36
wenzelm@20773
    37
val setup =
wenzelm@20773
    38
  Data.init #>
wenzelm@20773
    39
  Attrib.add_attributes [("atp", Attrib.add_del_args atp_add atp_del, "declaration of ATP rules")];
mengj@19159
    40
wenzelm@20547
    41
end;