src/HOL/IMPP/Misc.thy
changeset 63167 0909deb8059b
parent 62145 5b946c81dfbf
child 67613 ce654b0e6d69
--- a/src/HOL/IMPP/Misc.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/IMPP/Misc.thy	Thu May 26 17:51:22 2016 +0200
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, TUM
 *)
 
-section {* Several examples for Hoare logic *}
+section \<open>Several examples for Hoare logic\<close>
 
 theory Misc
 imports Hoare