--- a/src/HOL/Data_Structures/Tree23_Set.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Sat Jan 05 17:24:33 2019 +0100
@@ -208,7 +208,7 @@
subsubsection "Proofs for insert"
-text\<open>First a standard proof that @{const ins} preserves @{const bal}.\<close>
+text\<open>First a standard proof that \<^const>\<open>ins\<close> preserves \<^const>\<open>bal\<close>.\<close>
instantiation up\<^sub>i :: (type)height
begin
@@ -266,11 +266,9 @@
lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
by (auto elim!: bal_imp_full full_imp_bal)
-text \<open>The @{const "insert"} function either preserves the height of the
-tree, or increases it by one. The constructor returned by the @{term
-"insert"} function determines which: A return value of the form @{term
-"T\<^sub>i t"} indicates that the height will be the same. A value of the
-form @{term "Up\<^sub>i l p r"} indicates an increase in height.\<close>
+text \<open>The \<^const>\<open>insert\<close> function either preserves the height of the
+tree, or increases it by one. The constructor returned by the \<^term>\<open>insert\<close> function determines which: A return value of the form \<^term>\<open>T\<^sub>i t\<close> indicates that the height will be the same. A value of the
+form \<^term>\<open>Up\<^sub>i l p r\<close> indicates an increase in height.\<close>
fun full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
@@ -279,7 +277,7 @@
lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
by (induct rule: full.induct) (auto split: up\<^sub>i.split)
-text \<open>The @{const insert} operation preserves balance.\<close>
+text \<open>The \<^const>\<open>insert\<close> operation preserves balance.\<close>
lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
unfolding bal_iff_full insert_def