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.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)
```