--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat May 14 22:00:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 15 16:40:24 2011 +0200
@@ -798,7 +798,7 @@
fun clasimpset_rules_of ctxt =
let
- val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> rep_cs
+ val {safeIs, safeEs, hazIs, hazEs, ...} = ctxt |> claset_of |> Classical.rep_cs
val intros = Item_Net.content safeIs @ Item_Net.content hazIs
val elims = map Classical.classical_rule (Item_Net.content safeEs @ Item_Net.content hazEs)
val simps = ctxt |> simpset_of |> dest_ss |> #simps
--- a/src/Provers/blast.ML Sat May 14 22:00:24 2011 +0200
+++ b/src/Provers/blast.ML Sun May 15 16:40:24 2011 +0200
@@ -35,9 +35,6 @@
"no DETERM" flag would prevent proofs failing here.
*)
-(*Should be a type abbreviation?*)
-type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
-
signature BLAST_DATA =
sig
structure Classical: CLASSICAL
@@ -554,7 +551,7 @@
| toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u);
-fun netMkRules ctxt P vars (nps: netpair list) =
+fun netMkRules ctxt P vars (nps: Classical.netpair list) =
case P of
(Const ("*Goal*", _) $ G) =>
let val pG = mk_Trueprop (toTerm 2 G)
--- a/src/Provers/classical.ML Sat May 14 22:00:24 2011 +0200
+++ b/src/Provers/classical.ML Sun May 15 16:40:24 2011 +0200
@@ -18,11 +18,6 @@
addSbefore addSafter addbefore addafter
addD2 addE2 addSD2 addSE2;
-
-(*should be a type abbreviation in signature CLASSICAL*)
-type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
-type wrapper = (int -> tactic) -> (int -> tactic);
-
signature CLASSICAL_DATA =
sig
val imp_elim: thm (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *)
@@ -35,21 +30,8 @@
signature BASIC_CLASSICAL =
sig
+ type wrapper = (int -> tactic) -> int -> tactic
type claset
- val empty_cs: claset
- val merge_cs: claset * claset -> claset
- val rep_cs: claset ->
- {safeIs: thm Item_Net.T,
- safeEs: thm Item_Net.T,
- hazIs: thm Item_Net.T,
- hazEs: thm Item_Net.T,
- swrappers: (string * (Proof.context -> wrapper)) list,
- uwrappers: (string * (Proof.context -> wrapper)) list,
- safe0_netpair: netpair,
- safep_netpair: netpair,
- haz_netpair: netpair,
- dup_netpair: netpair,
- xtra_netpair: Context_Rules.netpair}
val print_claset: Proof.context -> unit
val addDs: Proof.context * thm list -> Proof.context
val addEs: Proof.context * thm list -> Proof.context
@@ -114,6 +96,19 @@
sig
include BASIC_CLASSICAL
val classical_rule: thm -> thm
+ type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
+ val rep_cs: claset ->
+ {safeIs: thm Item_Net.T,
+ safeEs: thm Item_Net.T,
+ hazIs: thm Item_Net.T,
+ hazEs: thm Item_Net.T,
+ swrappers: (string * (Proof.context -> wrapper)) list,
+ uwrappers: (string * (Proof.context -> wrapper)) list,
+ safe0_netpair: netpair,
+ safep_netpair: netpair,
+ haz_netpair: netpair,
+ dup_netpair: netpair,
+ xtra_netpair: Context_Rules.netpair}
val get_cs: Context.generic -> claset
val map_cs: (claset -> claset) -> Context.generic -> Context.generic
val safe_dest: int option -> attribute
@@ -213,6 +208,9 @@
(**** Classical rule sets ****)
+type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
+type wrapper = (int -> tactic) -> int -> tactic;
+
datatype claset =
CS of
{safeIs : thm Item_Net.T, (*safe introduction rules*)