| changeset 10171 | 59d6633835fa |
| parent 9933 | 9feb1e0c4cb3 |
| child 10795 | 9e888d60d3e5 |
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Mon Oct 09 09:33:45 2000 +0200 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Mon Oct 09 10:18:21 2000 +0200 @@ -92,7 +92,8 @@ *} apply(induct_tac b); -by(auto); +apply(auto); +done text{*\noindent In fact, all proofs in this case study look exactly like this. Hence we do