equal
deleted
inserted
replaced
108 \begin{isamarkuptxt}% |
108 \begin{isamarkuptxt}% |
109 \noindent |
109 \noindent |
110 The resulting 8 goals (one for each constructor) are proved in one fell swoop:% |
110 The resulting 8 goals (one for each constructor) are proved in one fell swoop:% |
111 \end{isamarkuptxt}% |
111 \end{isamarkuptxt}% |
112 \isamarkuptrue% |
112 \isamarkuptrue% |
113 \isacommand{apply}\ simp{\isacharunderscore}all\isanewline |
113 \isacommand{apply}\ simp{\isacharunderscore}all\isamarkupfalse% |
114 \isamarkupfalse% |
|
115 \isamarkupfalse% |
114 \isamarkupfalse% |
116 % |
115 % |
117 \begin{isamarkuptext}% |
116 \begin{isamarkuptext}% |
118 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
117 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
119 an inductive proof expects a goal of the form |
118 an inductive proof expects a goal of the form |