changeset 517 | d8c376662bb4 |
parent 359 | be6538c7b41d |
child 551 | be361e980acf |
--- 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 =