changeset 52230 | 1105b3b5aa77 |
parent 52143 | 36ffe23b25f8 |
child 55380 | 4de48353034e |
--- a/src/FOLP/IFOLP.thy Thu May 30 08:27:51 2013 +0200 +++ b/src/FOLP/IFOLP.thy Thu May 30 12:35:40 2013 +0200 @@ -292,8 +292,6 @@ done -(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) - schematic_lemma iffE: assumes "p:P <-> Q" and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R"