src/HOL/NatDef.ML

--- a/src/HOL/NatDef.ML	Fri May 30 15:24:27 1997 +0200
+++ b/src/HOL/NatDef.ML	Fri May 30 15:30:52 1997 +0200
@@ -203,6 +203,11 @@
 
 (*** Basic properties of "less than" ***)
 
+(*Used in TFL/post.sml*)
+goalw thy [less_def] "(m,n) : pred_nat^+ = (m<n)";
+by (rtac refl 1);
+qed "less_eq";
+
 (** Introduction properties **)
 
 val prems = goalw thy [less_def] "[| i<j;  j<k |] ==> i<(k::nat)";