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: