diff -r fb6c29a90003 -r d8c376662bb4 ProgTutorial/Package/Ind_General_Scheme.thy --- a/ProgTutorial/Package/Ind_General_Scheme.thy Mon Apr 30 12:36:32 2012 +0100 +++ b/ProgTutorial/Package/Ind_General_Scheme.thy Mon Apr 30 14:43:52 2012 +0100 @@ -197,7 +197,7 @@ \begin{figure}[p] \begin{minipage}{\textwidth} \begin{isabelle}*} -ML{*(* even-odd example *) +ML %grayML{*(* even-odd example *) val eo_defs = [@{thm even_def}, @{thm odd_def}] val eo_rules =