default rule step: norm_hhf_tac;
authorwenzelm
Sun Jan 29 19:23:41 2006 +0100 (2006-01-29)
changeset 188347e94af77cfce
parent 18833 bead1a4e966b
child 18835 8e080d0252c5
default rule step: norm_hhf_tac;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Sun Jan 29 19:23:40 2006 +0100
     1.2 +++ b/src/Provers/classical.ML	Sun Jan 29 19:23:41 2006 +0100
     1.3 @@ -1021,7 +1021,8 @@
     1.4    in
     1.5      Method.trace ctxt rules;
     1.6      fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
     1.7 -  end);
     1.8 +  end)
     1.9 +  THEN_ALL_NEW Tactic.norm_hhf_tac;
    1.10  
    1.11  fun rule_tac [] ctxt cs facts = some_rule_tac ctxt cs facts
    1.12    | rule_tac rules _ _ facts = Method.rule_tac rules facts;