--- a/src/Pure/tactic.ML Sun Oct 14 22:05:01 2001 +0200
+++ b/src/Pure/tactic.ML Sun Oct 14 22:05:46 2001 +0200
@@ -83,8 +83,9 @@
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 full_rewrite : thm list -> cterm -> thm
- val full_rewrite_cterm : thm list -> cterm -> cterm
+ val rewrite : bool -> thm list -> cterm -> thm
+ val rewrite_cterm : bool -> thm list -> cterm -> cterm
+ val simplify : bool -> thm list -> thm -> thm
val rewrite_goal_tac : thm list -> int -> tactic
val rewrite_goals_rule: thm list -> thm -> thm
val rewrite_rule : thm list -> thm -> thm
@@ -487,9 +488,10 @@
val simple_prover =
result1 (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss)));
-val full_rewrite = MetaSimplifier.full_rewrite_aux simple_prover;
-val full_rewrite_cterm = (#2 o Thm.dest_comb o #prop o Thm.crep_thm) oo full_rewrite;
-val rewrite_rule = MetaSimplifier.rewrite_rule_aux simple_prover;
+val rewrite = MetaSimplifier.rewrite_aux simple_prover;
+val rewrite_cterm = (#2 o Thm.dest_comb o #prop o Thm.crep_thm) ooo rewrite;
+val simplify = MetaSimplifier.simplify_aux simple_prover;
+val rewrite_rule = simplify true;
val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
(*Rewrite subgoal i only. SELECT_GOAL avoids inefficiencies in goals_conv.*)