diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Predicate_Compile_Examples/IMP_1.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Thu May 26 17:51:22 2016 +0200
@@ -2,11 +2,11 @@
 imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
 begin
 
-subsection {* IMP *}
+subsection \<open>IMP\<close>
 
-text {*
+text \<open>
   In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, and IF.
-*}
+\<close>
 
 type_synonym var = unit
 type_synonym state = bool