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