moved rewriting functions from Drule to MetaSimplifier
authorberghofe
Tue Nov 07 17:50:21 2000 +0100 (2000-11-07)
changeset 10415e6d7b77a0574
parent 10414 f7aeff3e9e1e
child 10416 5b33e732e459
moved rewriting functions from Drule to MetaSimplifier
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Tue Nov 07 17:48:25 2000 +0100
     1.2 +++ b/src/Pure/tactic.ML	Tue Nov 07 17:50:21 2000 +0100
     1.3 @@ -482,8 +482,8 @@
     1.4  val simple_prover =
     1.5    result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss)));
     1.6  
     1.7 -val rewrite_rule = Drule.rewrite_rule_aux simple_prover;
     1.8 -val rewrite_goals_rule = Drule.rewrite_goals_rule_aux simple_prover;
     1.9 +val rewrite_rule = MetaSimplifier.rewrite_rule_aux simple_prover;
    1.10 +val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
    1.11  
    1.12  
    1.13  (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)