diff -r 4daa384f4fd7 -r dc281bd5ca0a src/ZF/Nat.thy
--- 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
 {*