diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/Appendix.thy
--- a/ProgTutorial/Appendix.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Appendix.thy	Tue May 14 17:10:47 2019 +0200
@@ -3,12 +3,12 @@
 imports Base
 begin
 
-text {* \appendix *}
+text \<open>\appendix\<close>
 
 
-chapter {* Recipes *}
+chapter \<open>Recipes\<close>
 
-text {*
+text \<open>
   Possible topics: 
 
   \begin{itemize}
@@ -21,6 +21,6 @@
 
   \item Brief history of Isabelle
   \end{itemize}
-*}
+\<close>
 
 end