| changeset 10171 | 59d6633835fa |
| parent 9834 | 109b11c4e77e |
| child 10420 | ef006735bee8 |
--- a/doc-src/TutorialI/Misc/case_exprs.thy Mon Oct 09 09:33:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/case_exprs.thy Mon Oct 09 10:18:21 2000 +0200 @@ -65,8 +65,8 @@ which is solved automatically: *} -by(auto) - +apply(auto) +(*<*)done(*>*) text{* Note that we do not need to give a lemma a name if we do not intend to refer to it explicitly in the future.