
diff -r e9ab4ad7bd15 -r 23307fd33906 src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -206,7 +206,7 @@
 
 subsubsection "Proofs for insert"
 
-text{* First a standard proof that @{const ins} preserves @{const bal}. *}
+text\<open>First a standard proof that @{const ins} preserves @{const bal}.\<close>
 
 instantiation up\<^sub>i :: (type)height
 begin
@@ -222,8 +222,8 @@
 lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
 by (induct t) (auto split!: if_split up\<^sub>i.split) (* 15 secs in 2015 *)
 
-text{* Now an alternative proof (by Brian Huffman) that runs faster because
-two properties (balance and height) are combined in one predicate. *}
+text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
+two properties (balance and height) are combined in one predicate.\<close>
 
 inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
 "full 0 Leaf" |
@@ -264,11 +264,11 @@
 lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
   by (auto elim!: bal_imp_full full_imp_bal)
 
-text {* The @{const "insert"} function either preserves the height of the
+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. *}
+form @{term "Up\<^sub>i l p r"} 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" |
@@ -277,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 {* The @{const insert} operation preserves balance. *}
+text \<open>The @{const insert} operation preserves balance.\<close>
 
 lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
 unfolding bal_iff_full insert_def




