src/HOL/HOL.thy
changeset 59499 14095f771781
parent 59498 50b60f501b05
child 59507 b468e0f8da2a
     1.1 --- a/src/HOL/HOL.thy	Tue Feb 10 14:48:26 2015 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Feb 10 16:46:21 2015 +0100
     1.3 @@ -904,7 +904,8 @@
     1.4    shows R
     1.5  apply (rule ex1E [OF major])
     1.6  apply (rule prem)
     1.7 -apply (tactic {* ares_tac @{thms allI} 1 *})+
     1.8 +apply assumption
     1.9 +apply (rule allI)+
    1.10  apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{thm allE}] 1 *})
    1.11  apply iprover
    1.12  done