diff -r ee8e3eaad24c -r 1105b3b5aa77 src/FOLP/IFOLP.thy
--- 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"