src/ZF/ZF.thy

--- a/src/ZF/ZF.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/ZF/ZF.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -310,6 +310,8 @@
 lemma ballI [intro!]: "[| !!x. x\<in>A ==> P(x) |] ==> \<forall>x\<in>A. P(x)"
 by (simp add: Ball_def)
 
+lemmas strip = impI allI ballI
+
 lemma bspec [dest?]: "[| \<forall>x\<in>A. P(x);  x: A |] ==> P(x)"
 by (simp add: Ball_def)