equal
deleted
inserted
replaced
195 |
195 |
196 text_raw{* |
196 text_raw{* |
197 \begin{figure}[p] |
197 \begin{figure}[p] |
198 \begin{minipage}{\textwidth} |
198 \begin{minipage}{\textwidth} |
199 \begin{isabelle}*} |
199 \begin{isabelle}*} |
200 ML{*(* even-odd example *) |
200 ML %grayML{*(* even-odd example *) |
201 val eo_defs = [@{thm even_def}, @{thm odd_def}] |
201 val eo_defs = [@{thm even_def}, @{thm odd_def}] |
202 |
202 |
203 val eo_rules = |
203 val eo_rules = |
204 [@{prop "even 0"}, |
204 [@{prop "even 0"}, |
205 @{prop "\<And>n. odd n \<Longrightarrow> even (Suc n)"}, |
205 @{prop "\<And>n. odd n \<Longrightarrow> even (Suc n)"}, |