src/ZF/AC/Hartog.thy

--- a/src/ZF/AC/Hartog.thy	Wed Jul 10 16:07:52 2002 +0200
+++ b/src/ZF/AC/Hartog.thy	Wed Jul 10 16:54:07 2002 +0200
@@ -74,7 +74,7 @@
 
 lemma less_HartogE: "[| i < Hartog(A); i \<approx> Hartog(A) |] ==> P"
 by (blast intro: less_HartogE1 eqpoll_sym eqpoll_imp_lepoll 
-                 lepoll_trans [THEN Hartog_lepoll_selfE]);
+                 lepoll_trans [THEN Hartog_lepoll_selfE])
 
 lemma Card_Hartog: "Card(Hartog(A))"
 by (fast intro!: CardI Ord_Hartog elim: less_HartogE)