src/HOL/Induct/Comb.thy

 lemma Ap_reduce2 [intro]: "x \<rightarrow> y \<Longrightarrow> z\<bullet>x \<rightarrow> z\<bullet>y"
 apply (erule rtrancl_induct)
 apply (blast intro: rtrancl_trans)+
 done
 
-text \<open>Counterexample to the diamond property for @{term "x \<rightarrow>\<^sup>1 y"}\<close>
+text \<open>Counterexample to the diamond property for \<^term>\<open>x \<rightarrow>\<^sup>1 y\<close>\<close>
 
 lemma not_diamond_contract: "~ diamond(contract)"
 by (unfold diamond_def, metis S_contractE contract.K) 
 
 

 apply (erule parcontract.induct, fast+)
 done
 
 text \<open>
   \<^medskip>
-  Equivalence of @{prop "p \<rightarrow> q"} and @{prop "p \<Rrightarrow> q"}.
+  Equivalence of \<^prop>\<open>p \<rightarrow> q\<close> and \<^prop>\<open>p \<Rrightarrow> q\<close>.
 \<close>
 
 lemma contract_subset_parcontract: "contract \<subseteq> parcontract"
 by (auto, erule contract.induct, blast+)