src/HOL/NatArith.thy

--- a/src/HOL/NatArith.thy	Wed Jul 25 13:44:32 2001 +0200
+++ b/src/HOL/NatArith.thy	Wed Jul 25 17:58:26 2001 +0200
@@ -9,6 +9,11 @@
 
 setup arith_setup
 
+lemma pred_nat_trancl_eq_le: "(m, n) : pred_nat^* = (m <= n)"
+apply (simp add: less_eq reflcl_trancl [THEN sym] 
+            del: reflcl_trancl)
+by arith
+
 (*elimination of `-' on nat*)
 lemma nat_diff_split:
     "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"