src/HOL/Probability/Conditional_Expectation.thy
changeset 70125 b601c2c87076
parent 69712 dc85b5b3a532
child 70817 dd675800469d
     1.1 --- a/src/HOL/Probability/Conditional_Expectation.thy	Wed Apr 10 23:12:27 2019 +0100
     1.2 +++ b/src/HOL/Probability/Conditional_Expectation.thy	Thu Apr 11 15:26:04 2019 +0100
     1.3 @@ -994,7 +994,7 @@
     1.4    moreover have "real_cond_exp M F f x \<ge> c" if "\<forall>n. real_cond_exp M F f x > u n" for x
     1.5    proof -
     1.6      have "real_cond_exp M F f x \<ge> u n" for n using that less_imp_le by auto
     1.7 -    then show ?thesis using u(2) LIMSEQ_le_const2 by blast
     1.8 +    then show ?thesis using u(2) LIMSEQ_le_const2 by metis
     1.9    qed
    1.10    ultimately show ?thesis by auto
    1.11  qed