doc-src/TutorialI/Misc/arith2.thy
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  (*>*)