diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/SPARK/Manual/VC_Principles.thy
--- a/src/HOL/SPARK/Manual/VC_Principles.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/SPARK/Manual/VC_Principles.thy	Thu May 26 17:51:22 2016 +0200
@@ -4,9 +4,9 @@
 begin
 (*>*)
 
-chapter {* Principles of VC generation *}
+chapter \<open>Principles of VC generation\<close>
 
-text {*
+text \<open>
 \label{sec:vc-principles}
 In this section, we will discuss some aspects of VC generation that are
 useful for understanding and optimizing the VCs produced by the \SPARK{}
@@ -145,7 +145,7 @@
 The VC for the path from assertion 2 to assertion 1 is trivial, and so is the VC for the
 path from assertion 2 to the postcondition, expressing that the loop invariant implies
 the postcondition when the loop has terminated.
-*}
+\<close>
 
 (*<*)
 end