src/HOL/HOL.thy
changeset 59498 50b60f501b05
parent 59028 df7476e79558
child 59499 14095f771781
     1.1 --- a/src/HOL/HOL.thy	Tue Feb 10 14:29:36 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Feb 10 14:48:26 2015 +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 {* eresolve_tac [Classical.dup_elim NONE @{thm allE}] 1 *})
     1.8 +apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{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 (resolve_tac [Thm.unconstrainT @{thm eq_equal}]) *})
    1.17 +    by (tactic {* ALLGOALS (resolve_tac @{context} [Thm.unconstrainT @{thm eq_equal}]) *})
    1.18        (fact `PROP ?ofclass`)
    1.19  next
    1.20    assume "PROP ?equal"
    1.21 @@ -1923,7 +1923,7 @@
    1.22        let val conv = Code_Runtime.dynamic_holds_conv ctxt
    1.23        in
    1.24          CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
    1.25 -        resolve_tac [TrueI]
    1.26 +        resolve_tac ctxt [TrueI]
    1.27        end
    1.28    in
    1.29      Scan.succeed (SIMPLE_METHOD' o eval_tac)
    1.30 @@ -1935,7 +1935,7 @@
    1.31      SIMPLE_METHOD'
    1.32        (CHANGED_PROP o
    1.33          (CONVERSION (Nbe.dynamic_conv ctxt)
    1.34 -          THEN_ALL_NEW (TRY o resolve_tac [TrueI]))))
    1.35 +          THEN_ALL_NEW (TRY o resolve_tac ctxt [TrueI]))))
    1.36  *} "solve goal by normalization"
    1.37  
    1.38  
    1.39 @@ -1975,7 +1975,7 @@
    1.40      val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
    1.41    in
    1.42      fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
    1.43 -    fun smp_tac ctxt j = EVERY'[dresolve_tac (smp j), assume_tac ctxt];
    1.44 +    fun smp_tac ctxt j = EVERY' [dresolve_tac ctxt (smp j), assume_tac ctxt];
    1.45    end;
    1.46  
    1.47    local