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