--- 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)"