diff -r b98cd131e2b5 -r 5b5656a63bd6 src/HOL/ex/Tree23.thy
--- a/src/HOL/ex/Tree23.thy	Tue Oct 06 17:46:07 2015 +0200
+++ b/src/HOL/ex/Tree23.thy	Tue Oct 06 17:47:28 2015 +0200
@@ -2,13 +2,13 @@
     Author:     Tobias Nipkow, TU Muenchen
 *)
 
-section {* 2-3 Trees *}
+section \<open>2-3 Trees\<close>
 
 theory Tree23
 imports Main
 begin
 
-text{* This is a very direct translation of some of the functions in table.ML
+text\<open>This is a very direct translation of some of the functions in table.ML
 in the Isabelle source code. That source is due to Makarius Wenzel and Stefan
 Berghofer.
 
@@ -17,9 +17,9 @@
 
 Note that because of complicated patterns and mutual recursion, these
 function definitions take a few minutes and can also be seen as stress tests
-for the function definition facility.  *}
+for the function definition facility.\<close>
 
-type_synonym key = int -- {*for simplicity, should be a type class*}
+type_synonym key = int -- \<open>for simplicity, should be a type class\<close>
 
 datatype ord = LESS | EQUAL | GREATER
 
@@ -136,7 +136,7 @@
 definition del0 :: "key \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
 "del0 k t = (case del (Some k) t of None \<Rightarrow> t | Some(_,(_,t')) \<Rightarrow> t')"
 
-text {* Ordered trees *}
+text \<open>Ordered trees\<close>
 
 definition opt_less :: "key option \<Rightarrow> key option \<Rightarrow> bool" where
   "opt_less x y = (case x of None \<Rightarrow> True | Some a \<Rightarrow> (case y of None \<Rightarrow> True | Some b \<Rightarrow> a < b))"
@@ -155,7 +155,7 @@
 definition ord0 :: "'a tree23 \<Rightarrow> bool" where
   "ord0 t = ord' None t None"
 
-text {* Balanced trees *}
+text \<open>Balanced trees\<close>
 
 inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
 "full 0 Empty" |
@@ -189,7 +189,7 @@
 "height (Branch2 l _ r) = Suc(max (height l) (height r))" |
 "height (Branch3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
 
-text{* Is a tree balanced? *}
+text\<open>Is a tree balanced?\<close>
 fun bal :: "'a tree23 \<Rightarrow> bool" where
 "bal Empty = True" |
 "bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" |
@@ -207,11 +207,11 @@
 lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
   by (auto elim!: bal_imp_full full_imp_bal)
 
-text {* The @{term "add0"} function either preserves the height of the
+text \<open>The @{term "add0"} function either preserves the height of the
 tree, or increases it by one. The constructor returned by the @{term
 "add"} function determines which: A return value of the form @{term
 "Stay t"} indicates that the height will be the same. A value of the
-form @{term "Sprout l p r"} indicates an increase in height. *}
+form @{term "Sprout l p r"} indicates an increase in height.\<close>
 
 primrec gfull :: "nat \<Rightarrow> 'a growth \<Rightarrow> bool" where
 "gfull n (Stay t) \<longleftrightarrow> full n t" |
@@ -220,7 +220,7 @@
 lemma gfull_add: "full n t \<Longrightarrow> gfull n (add k y t)"
 by (induct set: full, auto split: ord.split growth.split)
 
-text {* The @{term "add0"} operation preserves balance. *}
+text \<open>The @{term "add0"} operation preserves balance.\<close>
 
 lemma bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)"
 unfolding bal_iff_full add0_def
@@ -230,7 +230,7 @@
 apply (auto intro: full.intros)
 done
 
-text {* The @{term "add0"} operation preserves order. *}
+text \<open>The @{term "add0"} operation preserves order.\<close>
 
 lemma ord_cases:
   fixes a b :: int obtains
@@ -279,7 +279,7 @@
 lemma ord0_add0: "ord0 t \<Longrightarrow> ord0 (add0 k y t)"
   by (simp add: ord0_def ord'_add0)
 
-text {* The @{term "del"} function preserves balance. *}
+text \<open>The @{term "del"} function preserves balance.\<close>
 
 lemma del_extra_simps:
 "l \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
@@ -409,8 +409,8 @@
 apply (rename_tac a, case_tac "a", rename_tac b t', case_tac "b", auto)
 done
 
-text{* This is a little test harness and should be commented out once the
-above functions have been proved correct. *}
+text\<open>This is a little test harness and should be commented out once the
+above functions have been proved correct.\<close>
 
 datatype 'a act = Add int 'a | Del int
 
@@ -419,7 +419,7 @@
 "exec (Add k x # as) t = exec as (add0 k x t)" |
 "exec (Del k # as) t = exec as (del0 k t)"
 
-text{* Some quick checks: *}
+text\<open>Some quick checks:\<close>
 
 lemma bal_exec: "bal t \<Longrightarrow> bal (exec as t)"
   by (induct as t arbitrary: t rule: exec.induct,