src/ZF/OrderArith.thy
changeset 61798 27f3c10b0b50
parent 60770 240563fbf41d
child 61980 6b780867d426
     1.1 --- a/src/ZF/OrderArith.thy	Mon Dec 07 10:19:30 2015 +0100
     1.2 +++ b/src/ZF/OrderArith.thy	Mon Dec 07 10:23:50 2015 +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 - --\<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)
    1.12 @@ -369,8 +369,8 @@
    1.13  apply blast
    1.14  done
    1.15  
    1.16 -text\<open>But note that the combination of @{text wf_imp_wf_on} and
    1.17 - @{text wf_rvimage} gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}\<close>
    1.18 +text\<open>But note that the combination of \<open>wf_imp_wf_on\<close> and
    1.19 + \<open>wf_rvimage\<close> gives @{prop "wf(r) ==> wf[C](rvimage(A,f,r))"}\<close>
    1.20  lemma wf_on_rvimage: "[| f \<in> A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
    1.21  apply (rule wf_onI2)
    1.22  apply (subgoal_tac "\<forall>z\<in>A. f`z=f`y \<longrightarrow> z \<in> Ba")
    1.23 @@ -460,7 +460,7 @@
    1.24  lemma wf_times: "A \<inter> B = 0 ==> wf(A*B)"
    1.25  by (simp add: wf_def, blast)
    1.26  
    1.27 -text\<open>Could also be used to prove @{text wf_radd}\<close>
    1.28 +text\<open>Could also be used to prove \<open>wf_radd\<close>\<close>
    1.29  lemma wf_Un:
    1.30       "[| range(r) \<inter> domain(s) = 0; wf(r);  wf(s) |] ==> wf(r \<union> s)"
    1.31  apply (simp add: wf_def, clarify)