equal
deleted
inserted
replaced
99 |
99 |
100 txt{*\noindent |
100 txt{*\noindent |
101 The resulting 8 goals (one for each constructor) are proved in one fell swoop: |
101 The resulting 8 goals (one for each constructor) are proved in one fell swoop: |
102 *} |
102 *} |
103 |
103 |
104 by simp_all; |
104 apply simp_all; |
|
105 (*<*)done(*>*) |
105 |
106 |
106 text{* |
107 text{* |
107 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
108 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
108 an inductive proof expects a goal of the form |
109 an inductive proof expects a goal of the form |
109 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |
110 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |