src/HOL/NatDef.ML
changeset 3378 11f4884a071a
parent 3355 0d955bcf8e0a
child 3457 a8ab7c64817c
     1.1 --- a/src/HOL/NatDef.ML	Fri May 30 15:24:27 1997 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Fri May 30 15:30:52 1997 +0200
     1.3 @@ -203,6 +203,11 @@
     1.4  
     1.5  (*** Basic properties of "less than" ***)
     1.6  
     1.7 +(*Used in TFL/post.sml*)
     1.8 +goalw thy [less_def] "(m,n) : pred_nat^+ = (m<n)";
     1.9 +by (rtac refl 1);
    1.10 +qed "less_eq";
    1.11 +
    1.12  (** Introduction properties **)
    1.13  
    1.14  val prems = goalw thy [less_def] "[| i<j;  j<k |] ==> i<(k::nat)";