changeset 58860 | fee7cfa69c50 |
parent 46953 | 2b6e55924af3 |
child 58871 | c399ae4b836f |
--- a/src/ZF/Trancl.thy Sat Nov 01 11:40:55 2014 +0100 +++ b/src/ZF/Trancl.thy Sat Nov 01 14:20:38 2014 +0100 @@ -90,7 +90,7 @@ lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)" by (unfold trans_def trans_on_def, blast) -lemma trans_on_imp_trans: "[|trans[A](r); r \<subseteq> A*A|] ==> trans(r)"; +lemma trans_on_imp_trans: "[|trans[A](r); r \<subseteq> A*A|] ==> trans(r)" by (simp add: trans_on_def trans_def, blast)