--- a/src/ZF/Nat.thy Thu May 29 17:10:00 2003 +0200
+++ b/src/ZF/Nat.thy Fri May 30 11:44:29 2003 +0200
@@ -290,6 +290,8 @@
apply (blast intro: lt_trans)
done
+lemma Le_iff [iff]: "<x,y> : Le <-> x le y & x : nat & y : nat"
+by (force simp add: Le_def)
ML
{*