src/HOL/Hoare/Hoare_Syntax.thy

--- a/src/HOL/Hoare/Hoare_Syntax.thy	Wed Dec 23 21:32:24 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Syntax.thy	Wed Dec 23 22:25:22 2020 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOL/Hoare/Hoare_Syntax.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Author:     Walter Guttmann (extension to total-correctness proofs)
+*)
 
-Concrete syntax for Hoare logic, with translations for variables.
-*)
+section \<open>Concrete syntax for Hoare logic, with translations for variables\<close>
 
 theory Hoare_Syntax
   imports Main