| changeset 12390 | 2fa13b499975 |
| parent 12156 | d2758965362e |
| child 13550 | 5a176b8dda84 |
--- a/doc-src/TutorialI/Rules/Forward.thy Wed Dec 05 14:32:10 2001 +0100 +++ b/doc-src/TutorialI/Rules/Forward.thy Wed Dec 05 15:36:36 2001 +0100 @@ -117,7 +117,7 @@ *} lemma "2 \<le> u \<Longrightarrow> u*m \<noteq> Suc(u*n)" -apply intro +apply (intro notI) txt{* before using arg_cong @{subgoals[display,indent=0,margin=65]}