Added in a signature.
authormengj
Thu Mar 02 00:57:34 2006 +0100 (2006-03-02)
changeset 19170a55a3464a1de
parent 19169 20a73345dd6e
child 19171 17b952ec5641
Added in a signature.
src/HOL/Tools/res_atpset.ML
     1.1 --- a/src/HOL/Tools/res_atpset.ML	Wed Mar 01 18:26:20 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atpset.ML	Thu Mar 02 00:57:34 2006 +0100
     1.3 @@ -4,7 +4,36 @@
     1.4  Set of rules used for ATPs
     1.5  *)
     1.6  
     1.7 -structure ResAtpSet =
     1.8 +signature RES_ATPSET =
     1.9 +sig
    1.10 +    type atpset
    1.11 +    val local_AtpSet_of: Proof.context -> atpset
    1.12 +    val add_atp_rules: atpset * Thm.thm list -> atpset
    1.13 +    val del_atp_rules: atpset * Thm.thm list -> atpset
    1.14 +    val get_AtpSet: theory -> atpset
    1.15 +    val print_local_AtpSet: Proof.context -> unit
    1.16 +    val AtpSet_of: theory -> atpset
    1.17 +    val add_atp_rule: Thm.thm * atpset -> atpset
    1.18 +    val del_atp_rule: Thm.thm * atpset -> atpset
    1.19 +    val print_atpset: atpset -> unit
    1.20 +    val setup: theory -> theory
    1.21 +    val get_local_AtpSet: Proof.context -> atpset
    1.22 +    val rep_as: atpset -> Thm.thm list
    1.23 +    val merge_atpset: atpset * atpset -> atpset
    1.24 +    val add_atp_rule': Thm.thm -> atpset -> atpset
    1.25 +    val del_atp_rule': Thm.thm -> atpset -> atpset
    1.26 +    val Add_AtpRs: Thm.thm list -> unit
    1.27 +    val Del_AtpRs: Thm.thm list -> unit
    1.28 +    val empty_atpset: atpset
    1.29 +    val put_local_AtpSet: atpset -> Proof.context -> Proof.context
    1.30 +    val print_AtpSet: theory -> unit
    1.31 +    val atp_rules_of_thy: theory -> Thm.thm list
    1.32 +    val atp_rules_of_ctxt: Proof.context -> Thm.thm list
    1.33 +end;
    1.34 +
    1.35 +
    1.36 +
    1.37 +structure ResAtpSet : RES_ATPSET =
    1.38  
    1.39  struct
    1.40  
    1.41 @@ -41,6 +70,7 @@
    1.42  	    |> Pretty.chunks |> Pretty.writeln
    1.43      end;
    1.44  
    1.45 +fun rep_as (AtpSet thms) = thms;
    1.46  
    1.47  (* global AtpSet *)
    1.48  
    1.49 @@ -70,6 +100,7 @@
    1.50  
    1.51  fun Del_AtpRs args = change_AtpSet (fn ars => del_atp_rules (ars,args));
    1.52  
    1.53 +fun atp_rules_of_thy thy = rep_as (AtpSet_of thy);
    1.54  
    1.55  (* local AtpSet *)
    1.56  
    1.57 @@ -87,8 +118,9 @@
    1.58  
    1.59  val put_local_AtpSet = LocalAtpSet.put;
    1.60  
    1.61 -fun local_AtpSet_of ctxt = get_local_AtpSet;
    1.62 +fun local_AtpSet_of ctxt = get_local_AtpSet ctxt;
    1.63  
    1.64 +fun atp_rules_of_ctxt ctxt = rep_as (local_AtpSet_of ctxt);
    1.65  
    1.66  (* attributes *)
    1.67  fun attrib f = Thm.declaration_attribute (fn th =>