src/ZF/OrdQuant.thy
changeset 13174 85d3c0981a16
parent 13172 03a5afa7b888
child 13175 81082cfa5618
     1.1 --- a/src/ZF/OrdQuant.thy	Wed May 22 18:55:47 2002 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Wed May 22 19:34:01 2002 +0200
     1.3 @@ -60,10 +60,6 @@
     1.4  
     1.5  (** Now some very basic ZF theorems **)
     1.6  
     1.7 -(*FIXME: move to ZF.thy or even to FOL.thy??*)
     1.8 -lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
     1.9 -by blast
    1.10 -
    1.11  (*FIXME: move to Rel.thy*)
    1.12  lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
    1.13  by (unfold trans_def trans_on_def, blast)