src/Provers/classical.ML
changeset 18834 7e94af77cfce
parent 18728 6790126ab5f6
child 18989 a5c3bc6fd6b6
     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;