src/HOL/arith_data.ML
changeset 5591 fbb4e1ac234d
parent 5553 ae42b36a50c2
child 5771 7c2c8cf20221
     1.1 --- a/src/HOL/arith_data.ML	Thu Oct 01 18:22:24 1998 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Thu Oct 01 18:23:00 1998 +0200
     1.3 @@ -230,5 +230,5 @@
     1.4  by (Clarify_tac 2);
     1.5  by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2);
     1.6  by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
     1.7 -				      Suc_diff_le]) 1);
     1.8 +				      Suc_diff_le, less_imp_le]) 1);
     1.9  qed_spec_mp "diff_less_mono2";