src/ZF/OrderArith.thy
changeset 67443 3abf6a722518
parent 61980 6b780867d426
child 69593 3dda49e08b9d
     1.1 --- a/src/ZF/OrderArith.thy	Tue Jan 16 09:12:16 2018 +0100
     1.2 +++ b/src/ZF/OrderArith.thy	Tue Jan 16 09:30:00 2018 +0100
     1.3 @@ -87,7 +87,7 @@
     1.4  lemma wf_on_radd: "[| wf[A](r);  wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"
     1.5  apply (rule wf_onI2)
     1.6  apply (subgoal_tac "\<forall>x\<in>A. Inl (x) \<in> Ba")
     1.7 - \<comment>\<open>Proving the lemma, which is needed twice!\<close>
     1.8 + \<comment> \<open>Proving the lemma, which is needed twice!\<close>
     1.9   prefer 2
    1.10   apply (erule_tac V = "y \<in> A + B" in thin_rl)
    1.11   apply (rule_tac ballI)