# HG changeset patch
# User wenzelm
# Date 1149189294 -7200
# Node ID 61c4117345c60372c9bdd7dd2904117bb9a24da9
# Parent  90f80de04c4609ffaa9623837211a7779df1d92a
lemmas strip;

diff -r 90f80de04c46 -r 61c4117345c6 src/FOL/IFOL.thy
--- 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)"