--- 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