src/ZF/Cardinal_AC.thy

 lemma cardinal_eqpoll: "|A| \<approx> A"
 apply (rule AC_well_ord [THEN exE])
 apply (erule well_ord_cardinal_eqpoll)
 done
 
-text\<open>The theorem @{term "||A|| = |A|"}\<close>
+text\<open>The theorem \<^term>\<open>||A|| = |A|\<close>\<close>
 lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp]
 
 lemma cardinal_eqE: "|X| = |Y| ==> X \<approx> Y"
 apply (rule AC_well_ord [THEN exE])
 apply (rule AC_well_ord [THEN exE])

   also have "... \<approx> K" 
     by (simp add: K InfCard_square_eq InfCard_is_Card Card_cardinal_eq)
   finally show "(\<Union>i\<in>K. X(i)) \<lesssim> K" .
 qed
 
-text\<open>The same again, using @{term csucc}\<close>
+text\<open>The same again, using \<^term>\<open>csucc\<close>\<close>
 lemma cardinal_UN_lt_csucc:
      "[| InfCard(K);  \<And>i. i\<in>K \<Longrightarrow> |X(i)| < csucc(K) |]
       ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
 by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
 

 
 
 subsection\<open>The Main Result for Infinite-Branching Datatypes\<close>
 
 text\<open>As above, but the index set need not be a cardinal. Work
-backwards along the injection from @{term W} into @{term K}, given
-that @{term"W\<noteq>0"}.\<close>
+backwards along the injection from \<^term>\<open>W\<close> into \<^term>\<open>K\<close>, given
+that \<^term>\<open>W\<noteq>0\<close>.\<close>
 
 lemma inj_UN_subset:
   assumes f: "f \<in> inj(A,B)" and a: "a \<in> A"
   shows "(\<Union>x\<in>A. C(x)) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))"
 proof (rule UN_least)