--- a/src/Provers/blast.ML Tue Sep 21 17:26:42 1999 +0200
+++ b/src/Provers/blast.ML Tue Sep 21 17:26:50 1999 +0200
@@ -68,7 +68,7 @@
safe0_netpair: netpair, safep_netpair: netpair,
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
- val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
+ val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
end;
@@ -1330,11 +1330,11 @@
(** method setup **)
-val blast_args =
- Method.sectioned_args (K (Scan.lift (Scan.option Args.nat))) Data.cla_modifiers;
+fun blast_args m =
+ Method.sectioned_args (K (Args.bang_facts -- Scan.lift (Scan.option Args.nat))) Data.cla_modifiers m;
-fun blast_meth None = Data.cla_meth' blast_tac
- | blast_meth (Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
+fun blast_meth (prems, None) = Data.cla_meth' blast_tac prems
+ | blast_meth (prems, Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim) prems;
val setup = [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]];
--- a/src/Provers/clasimp.ML Tue Sep 21 17:26:42 1999 +0200
+++ b/src/Provers/clasimp.ML Tue Sep 21 17:26:50 1999 +0200
@@ -153,16 +153,15 @@
(Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
val clasimp_modifiers = Classical.cla_modifiers @ Simplifier.simp_modifiers;
-val clasimp_args = Method.only_sectioned_args clasimp_modifiers;
-fun clasimp_meth tac ctxt = Method.METHOD (fn facts =>
- ALLGOALS (Method.insert_tac facts) THEN tac (get_local_clasimpset ctxt));
+fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
+ ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
-fun clasimp_meth' tac ctxt = Method.METHOD (fn facts =>
- FIRSTGOAL (Method.insert_tac facts THEN' tac (get_local_clasimpset ctxt)));
+fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
+ FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
-val clasimp_method = clasimp_args o clasimp_meth;
-val clasimp_method' = clasimp_args o clasimp_meth';
+val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
+val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
val setup =
--- a/src/Provers/classical.ML Tue Sep 21 17:26:42 1999 +0200
+++ b/src/Provers/classical.ML Tue Sep 21 17:26:50 1999 +0200
@@ -162,8 +162,8 @@
val xtra_intro_local: Proof.context attribute
val delrule_local: Proof.context attribute
val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
- val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
- val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
+ val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
+ val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
val setup: (theory -> theory) list
@@ -347,7 +347,7 @@
cs)
else
let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
- partition (fn rl => nprems_of rl=0) [th]
+ partition Thm.no_prems [th]
val nI = length safeIs + 1
and nE = length safeEs
in warn_dup th cs;
@@ -530,7 +530,7 @@
(cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm (th, safeIs) then
- let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th]
+ let val (safe0_rls, safep_rls) = partition Thm.no_prems [th]
in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
safep_netpair = delete (safep_rls, []) safep_netpair,
safeIs = rem_thm (safeIs,th),
@@ -1145,16 +1145,14 @@
Args.$$$ introN >> K (I, safe_intro_local),
Args.$$$ delN >> K (I, delrule_local)];
-val cla_args = Method.only_sectioned_args cla_modifiers;
-
-fun cla_meth tac ctxt = Method.METHOD (fn facts =>
- ALLGOALS (Method.insert_tac facts) THEN tac (get_local_claset ctxt));
+fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
+ ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
-fun cla_meth' tac ctxt = Method.METHOD (fn facts =>
- FIRSTGOAL (Method.insert_tac facts THEN' tac (get_local_claset ctxt)));
+fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
+ FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
-val cla_method = cla_args o cla_meth;
-val cla_method' = cla_args o cla_meth';
+val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
+val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';