diff -r fef1df4268d6 -r be4d203d35b3 src/HOL/Hoare_Parallel/RG_Examples.thy --- a/src/HOL/Hoare_Parallel/RG_Examples.thy Sun Nov 02 17:27:22 2014 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Sun Nov 02 17:36:52 2014 +0100 @@ -1,4 +1,4 @@ -header {* \section{Examples} *} +section {* Examples *} theory RG_Examples imports RG_Syntax