lemmas strip;

--- a/src/FOL/IFOL.thy	Thu Jun 01 21:14:05 2006 +0200
+++ b/src/FOL/IFOL.thy	Thu Jun 01 21:14:54 2006 +0200
@@ -117,6 +117,9 @@
   iff_reflection: "(P<->Q) ==> (P==Q)"
 
 
+lemmas strip = impI allI
+
+
 text{*Thanks to Stephan Merz*}
 theorem subst:
   assumes eq: "a = b" and p: "P(a)"