--- 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";