changeset 10171 | 59d6633835fa |
parent 9458 | c613cd06d5cf |
1.1 --- a/doc-src/TutorialI/Misc/arith2.thy Mon Oct 09 09:33:45 2000 +0200 1.2 +++ b/doc-src/TutorialI/Misc/arith2.thy Mon Oct 09 10:18:21 2000 +0200 1.3 @@ -2,7 +2,8 @@ 1.4 theory arith2 = Main:; 1.5 (*>*) 1.6 lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))"; 1.7 -by(arith); 1.8 +apply(arith); 1.9 (**)(*<*) 1.10 +done 1.11 end 1.12 (*>*)