# HG changeset patch
# User paulson
# Date 864999052 -7200
# Node ID 11f4884a071a3a864caa6bb944a7a3f7620e51bb
# Parent  afa1fedef73f441f84555e9661cf3e3d7a226dda
Moved "less_eq" to NatDef from Arith

diff -r afa1fedef73f -r 11f4884a071a 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)";