equal
deleted
inserted
replaced
305 % |
305 % |
306 \begin{isamarkuptext}% |
306 \begin{isamarkuptext}% |
307 \noindent The datatype induction rule generated here is of the form |
307 \noindent The datatype induction rule generated here is of the form |
308 \begin{isabelle}% |
308 \begin{isabelle}% |
309 \ {\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline |
309 \ {\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline |
310 \isaindent{\ \ \ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline |
310 \isaindent{\ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline |
311 \isaindent{\ \ \ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline |
311 \isaindent{\ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline |
312 \isaindent{\ }{\isasymLongrightarrow}\ P\ bintree% |
312 \isaindent{\ }{\isasymLongrightarrow}\ P\ bintree% |
313 \end{isabelle}% |
313 \end{isabelle}% |
314 \end{isamarkuptext}% |
314 \end{isamarkuptext}% |
315 \isamarkuptrue% |
315 \isamarkuptrue% |
316 % |
316 % |