--- a/src/HOL/Import/HOL/HOL4Base.thy Thu Sep 29 17:09:11 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy Thu Sep 29 18:01:12 2005 +0200
@@ -1469,9 +1469,6 @@
lemma LESS_EQUAL_ADD: "ALL (m::nat) n::nat. m <= n --> (EX p::nat. n = m + p)"
by (import arithmetic LESS_EQUAL_ADD)
-lemma LESS_EQ_EXISTS: "ALL (m::nat) n::nat. (m <= n) = (EX p::nat. n = m + p)"
- by (import arithmetic LESS_EQ_EXISTS)
-
lemma MULT_EQ_1: "ALL (x::nat) y::nat. (x * y = 1) = (x = 1 & y = 1)"
by (import arithmetic MULT_EQ_1)