src/HOL/Old_Number_Theory/WilsonBij.thy
changeset 32960 69916a850301
parent 32479 521cc9bf2958
child 35048 82ab78fff970
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -155,7 +155,7 @@
                apply (rule_tac [7] inv_g_1 [THEN aux2])
                  apply (unfold zprime_def)
                  apply (auto intro: d22set_g_1 d22set_le
-		   aux1 aux2 aux3 aux4)
+                   aux1 aux2 aux3 aux4)
   done
 
 lemma inv_d22set_d22set: