src/Provers/blast.ML
changeset 58838 59203adfc33f
parent 58826 2ed2eaabe3df
child 58950 d07464875dd4
     1.1 --- a/src/Provers/blast.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/Provers/blast.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -488,8 +488,8 @@
     1.4  
     1.5  (*Resolution/matching tactics: if upd then the proof state may be updated.
     1.6    Matching makes the tactics more deterministic in the presence of Vars.*)
     1.7 -fun emtac ctxt upd rl = TRACE ctxt rl (if upd then etac rl else ematch_tac [rl]);
     1.8 -fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then rtac rl else match_tac [rl]);
     1.9 +fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac [rl]);
    1.10 +fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac [rl]);
    1.11  
    1.12  (*Tableau rule from elimination rule.
    1.13    Flag "upd" says that the inference updated the branch.
    1.14 @@ -624,7 +624,7 @@
    1.15  
    1.16  (*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
    1.17  fun negOfGoal_tac ctxt i =
    1.18 -  TRACE ctxt Data.ccontr (rtac Data.ccontr) i THEN rotate_tac ~1 i;
    1.19 +  TRACE ctxt Data.ccontr (resolve_tac [Data.ccontr]) i THEN rotate_tac ~1 i;
    1.20  
    1.21  fun traceTerm ctxt t =
    1.22    let val thy = Proof_Context.theory_of ctxt