src/HOL/Arith.ML
changeset 3842 b55686a7b22c
parent 3724 f33e301a89f5
child 3896 ee8ebb74ec00
     1.1 --- a/src/HOL/Arith.ML	Fri Oct 10 18:37:49 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Oct 10 19:02:28 1997 +0200
     1.3 @@ -255,7 +255,7 @@
     1.4  
     1.5  (*non-strict, in 1st argument*)
     1.6  goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k";
     1.7 -by (res_inst_tac [("f", "%j.j+k")] less_mono_imp_le_mono 1);
     1.8 +by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
     1.9  by (etac add_less_mono1 1);
    1.10  by (assume_tac 1);
    1.11  qed "add_le_mono1";