src/Provers/classical.ML
changeset 42812 dda4aef7cba4
parent 42810 2425068fe13a
child 42817 7e819eb7dabb
     1.1 --- a/src/Provers/classical.ML	Sat May 14 22:00:24 2011 +0200
     1.2 +++ b/src/Provers/classical.ML	Sun May 15 16:40:24 2011 +0200
     1.3 @@ -18,11 +18,6 @@
     1.4    addSbefore addSafter addbefore addafter
     1.5    addD2 addE2 addSD2 addSE2;
     1.6  
     1.7 -
     1.8 -(*should be a type abbreviation in signature CLASSICAL*)
     1.9 -type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
    1.10 -type wrapper = (int -> tactic) -> (int -> tactic);
    1.11 -
    1.12  signature CLASSICAL_DATA =
    1.13  sig
    1.14    val imp_elim: thm  (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *)
    1.15 @@ -35,21 +30,8 @@
    1.16  
    1.17  signature BASIC_CLASSICAL =
    1.18  sig
    1.19 +  type wrapper = (int -> tactic) -> int -> tactic
    1.20    type claset
    1.21 -  val empty_cs: claset
    1.22 -  val merge_cs: claset * claset -> claset
    1.23 -  val rep_cs: claset ->
    1.24 -   {safeIs: thm Item_Net.T,
    1.25 -    safeEs: thm Item_Net.T,
    1.26 -    hazIs: thm Item_Net.T,
    1.27 -    hazEs: thm Item_Net.T,
    1.28 -    swrappers: (string * (Proof.context -> wrapper)) list,
    1.29 -    uwrappers: (string * (Proof.context -> wrapper)) list,
    1.30 -    safe0_netpair: netpair,
    1.31 -    safep_netpair: netpair,
    1.32 -    haz_netpair: netpair,
    1.33 -    dup_netpair: netpair,
    1.34 -    xtra_netpair: Context_Rules.netpair}
    1.35    val print_claset: Proof.context -> unit
    1.36    val addDs: Proof.context * thm list -> Proof.context
    1.37    val addEs: Proof.context * thm list -> Proof.context
    1.38 @@ -114,6 +96,19 @@
    1.39  sig
    1.40    include BASIC_CLASSICAL
    1.41    val classical_rule: thm -> thm
    1.42 +  type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
    1.43 +  val rep_cs: claset ->
    1.44 +   {safeIs: thm Item_Net.T,
    1.45 +    safeEs: thm Item_Net.T,
    1.46 +    hazIs: thm Item_Net.T,
    1.47 +    hazEs: thm Item_Net.T,
    1.48 +    swrappers: (string * (Proof.context -> wrapper)) list,
    1.49 +    uwrappers: (string * (Proof.context -> wrapper)) list,
    1.50 +    safe0_netpair: netpair,
    1.51 +    safep_netpair: netpair,
    1.52 +    haz_netpair: netpair,
    1.53 +    dup_netpair: netpair,
    1.54 +    xtra_netpair: Context_Rules.netpair}
    1.55    val get_cs: Context.generic -> claset
    1.56    val map_cs: (claset -> claset) -> Context.generic -> Context.generic
    1.57    val safe_dest: int option -> attribute
    1.58 @@ -213,6 +208,9 @@
    1.59  
    1.60  (**** Classical rule sets ****)
    1.61  
    1.62 +type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
    1.63 +type wrapper = (int -> tactic) -> int -> tactic;
    1.64 +
    1.65  datatype claset =
    1.66    CS of
    1.67     {safeIs         : thm Item_Net.T,          (*safe introduction rules*)