src/Provers/classical.ML
changeset 58838 59203adfc33f
parent 58826 2ed2eaabe3df
child 58893 9e0ecb66d6a7
     1.1 --- a/src/Provers/classical.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/Provers/classical.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -157,7 +157,7 @@
     1.4        val rule'' =
     1.5          rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
     1.6            if i = 1 orelse redundant_hyp goal
     1.7 -          then etac thin_rl i
     1.8 +          then eresolve_tac [thin_rl] i
     1.9            else all_tac))
    1.10          |> Seq.hd
    1.11          |> Drule.zero_var_indexes;
    1.12 @@ -209,7 +209,7 @@
    1.13    let
    1.14      val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
    1.15      val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
    1.16 -  in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
    1.17 +  in rule_by_tactic ctxt (TRYALL (eresolve_tac [revcut_rl])) rl end;
    1.18  
    1.19  
    1.20  (**** Classical rule sets ****)
    1.21 @@ -689,8 +689,8 @@
    1.22  fun ctxt addafter (name, tac2) =
    1.23    ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt);
    1.24  
    1.25 -fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dtac thm THEN' assume_tac);
    1.26 -fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => etac thm THEN' assume_tac);
    1.27 +fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
    1.28 +fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
    1.29  fun ctxt addSD2 (name, thm) = ctxt addSafter (name, fn _ => dmatch_tac [thm] THEN' eq_assume_tac);
    1.30  fun ctxt addSE2 (name, thm) = ctxt addSafter (name, fn _ => ematch_tac [thm] THEN' eq_assume_tac);
    1.31  
    1.32 @@ -909,7 +909,7 @@
    1.33      val ruleq = Drule.multi_resolves facts rules;
    1.34      val _ = Method.trace ctxt rules;
    1.35    in
    1.36 -    fn st => Seq.maps (fn rule => rtac rule i st) ruleq
    1.37 +    fn st => Seq.maps (fn rule => resolve_tac [rule] i st) ruleq
    1.38    end)
    1.39    THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
    1.40