--- a/src/HOL/Induct/QuoDataType.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Induct/QuoDataType.thy Sat Jan 05 17:24:33 2019 +0100
@@ -115,7 +115,7 @@
| "freediscrim (CRYPT K X) = freediscrim X + 2"
| "freediscrim (DECRYPT K X) = freediscrim X - 2"
-text\<open>This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}\<close>
+text\<open>This theorem helps us prove \<^term>\<open>Nonce N \<noteq> MPair X Y\<close>\<close>
theorem msgrel_imp_eq_freediscrim:
"U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
by (induct set: msgrel) auto
@@ -151,8 +151,8 @@
Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
-text\<open>Reduces equality of equivalence classes to the @{term msgrel} relation:
- @{term "(msgrel `` {x} = msgrel `` {y}) = ((x,y) \<in> msgrel)"}\<close>
+text\<open>Reduces equality of equivalence classes to the \<^term>\<open>msgrel\<close> relation:
+ \<^term>\<open>(msgrel `` {x} = msgrel `` {y}) = ((x,y) \<in> msgrel)\<close>\<close>
lemmas equiv_msgrel_iff = eq_equiv_class_iff [OF equiv_msgrel UNIV_I UNIV_I]
declare equiv_msgrel_iff [simp]
@@ -227,7 +227,7 @@
by (auto simp add: congruent_def msgrel_imp_eq_freenonces)
-text\<open>Now prove the four equations for @{term nonces}\<close>
+text\<open>Now prove the four equations for \<^term>\<open>nonces\<close>\<close>
lemma nonces_Nonce [simp]: "nonces (Nonce N) = {N}"
by (simp add: nonces_def Nonce_def
@@ -261,7 +261,7 @@
lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
by (auto simp add: congruent_def msgrel_imp_eqv_freeleft)
-text\<open>Now prove the four equations for @{term left}\<close>
+text\<open>Now prove the four equations for \<^term>\<open>left\<close>\<close>
lemma left_Nonce [simp]: "left (Nonce N) = Nonce N"
by (simp add: left_def Nonce_def
@@ -295,7 +295,7 @@
lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
by (auto simp add: congruent_def msgrel_imp_eqv_freeright)
-text\<open>Now prove the four equations for @{term right}\<close>
+text\<open>Now prove the four equations for \<^term>\<open>right\<close>\<close>
lemma right_Nonce [simp]: "right (Nonce N) = Nonce N"
by (simp add: right_def Nonce_def
@@ -325,7 +325,7 @@
lemma NONCE_imp_eq: "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
by (drule msgrel_imp_eq_freenonces, simp)
-text\<open>Can also be proved using the function @{term nonces}\<close>
+text\<open>Can also be proved using the function \<^term>\<open>nonces\<close>\<close>
lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)"
by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq)
@@ -430,7 +430,7 @@
lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
by (auto simp add: congruent_def msgrel_imp_eq_freediscrim)
-text\<open>Now prove the four equations for @{term discrim}\<close>
+text\<open>Now prove the four equations for \<^term>\<open>discrim\<close>\<close>
lemma discrim_Nonce [simp]: "discrim (Nonce N) = 0"
by (simp add: discrim_def Nonce_def