diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/Package/Ind_Intro.thy --- 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 \How to Write a Definitional Package\label{chp:package}\ -text {* +text \ \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. -*} +\ end