src/HOL/HOL.thy
changeset 58839 ccda99401bc8
parent 58830 e05c620eceeb
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/HOL.thy	Thu Oct 30 16:55:29 2014 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Oct 30 22:45:19 2014 +0100
     1.3 @@ -905,7 +905,7 @@
     1.4  apply (rule ex1E [OF major])
     1.5  apply (rule prem)
     1.6  apply (tactic {* ares_tac @{thms allI} 1 *})+
     1.7 -apply (tactic {* etac (Classical.dup_elim @{thm allE}) 1 *})
     1.8 +apply (tactic {* eresolve_tac [Classical.dup_elim @{thm allE}] 1 *})
     1.9  apply iprover
    1.10  done
    1.11  
    1.12 @@ -1822,7 +1822,7 @@
    1.13  proof
    1.14    assume "PROP ?ofclass"
    1.15    show "PROP ?equal"
    1.16 -    by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm eq_equal})) *})
    1.17 +    by (tactic {* ALLGOALS (resolve_tac [Thm.unconstrainT @{thm eq_equal}]) *})
    1.18        (fact `PROP ?ofclass`)
    1.19  next
    1.20    assume "PROP ?equal"
    1.21 @@ -1921,7 +1921,10 @@
    1.22    let
    1.23      fun eval_tac ctxt =
    1.24        let val conv = Code_Runtime.dynamic_holds_conv ctxt
    1.25 -      in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
    1.26 +      in
    1.27 +        CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
    1.28 +        resolve_tac [TrueI]
    1.29 +      end
    1.30    in
    1.31      Scan.succeed (SIMPLE_METHOD' o eval_tac)
    1.32    end
    1.33 @@ -1932,7 +1935,7 @@
    1.34      SIMPLE_METHOD'
    1.35        (CHANGED_PROP o
    1.36          (CONVERSION (Nbe.dynamic_conv ctxt)
    1.37 -          THEN_ALL_NEW (TRY o rtac TrueI))))
    1.38 +          THEN_ALL_NEW (TRY o resolve_tac [TrueI]))))
    1.39  *} "solve goal by normalization"
    1.40  
    1.41  
    1.42 @@ -1979,7 +1982,7 @@
    1.43      val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
    1.44    in
    1.45      fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
    1.46 -    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
    1.47 +    fun smp_tac j = EVERY'[dresolve_tac (smp j), assume_tac];
    1.48    end;
    1.49  
    1.50    local