src/ZF/Arith.thy

--- a/src/ZF/Arith.thy	Sun Nov 20 21:07:10 2011 +0100
+++ b/src/ZF/Arith.thy	Sun Nov 20 21:28:07 2011 +0100
@@ -88,7 +88,7 @@
 done
 
 (* [| 0 < k; k \<in> nat; !!j. [| j \<in> nat; k = succ(j) |] ==> Q |] ==> Q *)
-lemmas zero_lt_natE = zero_lt_lemma [THEN bexE, standard]
+lemmas zero_lt_natE = zero_lt_lemma [THEN bexE]
 
 
 subsection{*@{text natify}, the Coercion to @{term nat}*}