--- a/src/Pure/tactic.ML Thu Jul 24 15:25:29 1997 +0200
+++ b/src/Pure/tactic.ML Fri Jul 25 11:47:09 1997 +0200
@@ -1,4 +1,4 @@
-(* Title: tactic
+(* Title: Pure/tactic.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -72,6 +72,8 @@
val resolve_from_net_tac : (int*thm) Net.net -> int -> tactic
val resolve_tac : thm list -> int -> tactic
val res_inst_tac : (string*string)list -> thm -> int -> tactic
+ val rewrite_goals_rule: thm list -> thm -> thm
+ val rewrite_rule : thm list -> thm -> thm
val rewrite_goals_tac : thm list -> tactic
val rewrite_tac : thm list -> tactic
val rewtac : thm -> tactic
@@ -473,6 +475,13 @@
fun result1 tacf mss thm =
apsome fst (Sequence.pull (tacf mss thm));
+val simple_prover =
+ result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss)));
+
+val rewrite_rule = Drule.rewrite_rule_aux simple_prover;
+val rewrite_goals_rule = Drule.rewrite_goals_rule_aux simple_prover;
+
+
(*Rewrite subgoal i only. SELECT_GOAL avoids inefficiencies in goals_conv.*)
fun asm_rewrite_goal_tac mode prover_tac mss =
SELECT_GOAL