diff -r e9ab4ad7bd15 -r 23307fd33906 src/HOL/IMP/Hoare_Examples.thy
--- a/src/HOL/IMP/Hoare_Examples.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/HOL/IMP/Hoare_Examples.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -4,7 +4,7 @@
 
 hide_const (open) sum
 
-text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
+text\<open>Summing up the first @{text x} natural numbers in variable @{text y}.\<close>
 
 fun sum :: "int \<Rightarrow> int" where
 "sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)"
@@ -22,9 +22,9 @@
       ''x'' ::= Plus (V ''x'') (N (- 1)))"
 
 
-subsubsection{* Proof by Operational Semantics *}
+subsubsection\<open>Proof by Operational Semantics\<close>
 
-text{* The behaviour of the loop is proved by induction: *}
+text\<open>The behaviour of the loop is proved by induction:\<close>
 
 lemma while_sum:
   "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')"
@@ -32,12 +32,12 @@
 apply(auto)
 done
 
-text{* We were lucky that the proof was automatic, except for the
+text\<open>We were lucky that the proof was automatic, except for the
 induction. In general, such proofs will not be so easy. The automation is
 partly due to the right inversion rules that we set up as automatic
 elimination rules that decompose big-step premises.
 
-Now we prefix the loop with the necessary initialization: *}
+Now we prefix the loop with the necessary initialization:\<close>
 
 lemma sum_via_bigstep:
   assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t"
@@ -48,10 +48,10 @@
 qed
 
 
-subsubsection{* Proof by Hoare Logic *}
+subsubsection\<open>Proof by Hoare Logic\<close>
 
-text{* Note that we deal with sequences of commands from right to left,
-pulling back the postcondition towards the precondition. *}
+text\<open>Note that we deal with sequences of commands from right to left,
+pulling back the postcondition towards the precondition.\<close>
 
 lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}"
 apply(rule Seq)
@@ -67,11 +67,11 @@
 apply simp
 done
 
-text{* The proof is intentionally an apply script because it merely composes
+text\<open>The proof is intentionally an apply script because it merely composes
 the rules of Hoare logic. Of course, in a few places side conditions have to
 be proved. But since those proofs are 1-liners, a structured proof is
 overkill. In fact, we shall learn later that the application of the Hoare
 rules can be automated completely and all that is left for the user is to
-provide the loop invariants and prove the side-conditions. *}
+provide the loop invariants and prove the side-conditions.\<close>
 
 end