| changeset 10171 | 59d6633835fa |
| parent 9933 | 9feb1e0c4cb3 |
| child 10795 | 9e888d60d3e5 |
| 10170:dfff821d2949 | 10171:59d6633835fa |
|---|---|
90 txt{*\noindent |
90 txt{*\noindent |
91 The proof is canonical: |
91 The proof is canonical: |
92 *} |
92 *} |
93 |
93 |
94 apply(induct_tac b); |
94 apply(induct_tac b); |
95 by(auto); |
95 apply(auto); |
96 done |
|
96 |
97 |
97 text{*\noindent |
98 text{*\noindent |
98 In fact, all proofs in this case study look exactly like this. Hence we do |
99 In fact, all proofs in this case study look exactly like this. Hence we do |
99 not show them below. |
100 not show them below. |
100 |
101 |