src/ZF/AC/AC7_AC9.thy
changeset 32960 69916a850301
parent 27678 85ea2be46c71
child 46822 95f1e700b712
--- a/src/ZF/AC/AC7_AC9.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/ZF/AC/AC7_AC9.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      ZF/AC/AC7_AC9.thy
-    ID:         $Id$
     Author:     Krzysztof Grabczewski
 
 The proofs needed to state that AC7, AC8 and AC9 are equivalent to the previous
@@ -77,7 +76,7 @@
 apply (rule AC7_AC6_lemma1)
 apply (erule allE) 
 apply (blast del: notI
-	     intro!: AC7_AC6_lemma2 intro: eqpoll_sym eqpoll_trans 
+             intro!: AC7_AC6_lemma2 intro: eqpoll_sym eqpoll_trans 
                     Sigma_fun_space_eqpoll)
 done