diff -r 4e8837255b87 -r fe887910e32e src/HOL/UNITY/LessThan.ML
--- a/src/HOL/UNITY/LessThan.ML	Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/LessThan.ML	Thu Oct 15 11:35:07 1998 +0200
@@ -7,6 +7,7 @@
 *)
 
 
+(*Make Auto_tac and Force_tac try trans_tac!*)
 claset_ref() := claset() addaltern ("trans_tac",trans_tac);
 
 
@@ -27,6 +28,10 @@
 by (Blast_tac 1);
 qed "lessThan_Suc";
 
+Goalw [lessThan_def, atMost_def] "lessThan (Suc k) = atMost k";
+by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
+qed "lessThan_Suc_atMost";
+
 Goal "(UN m. lessThan m) = UNIV";
 by (Blast_tac 1);
 qed "UN_lessThan_UNIV";