src/ZF/Trancl.thy
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)