--- a/ProgTutorial/Package/Ind_Intro.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Package/Ind_Intro.thy	Tue May 14 17:10:47 2019 +0200
@@ -3,9 +3,9 @@
 begin
 
 
-chapter {* How to Write a Definitional Package\label{chp:package} *}
+chapter \<open>How to Write a Definitional Package\label{chp:package}\<close>
 
-text {*
+text \<open>
    \begin{flushright}
   {\em
   ``We will most likely never realize the full importance of painting the Tower,\\ 
@@ -44,6 +44,6 @@
   Moreover, it only proves a weaker form of the induction principle for inductive
   predicates. But it illustrates the implementation pf a typical package in
   Isabelle.
-*}
+\<close>
 
 end