# HG changeset patch
# User nipkow
# Date 1245577826 -7200
# Node ID 052399f580cfe701625c16b8248aa61a9532c573
# Parent  7ffc1a901eea94b14aa12df95fdb7f44186c2311
fixed proof

diff -r 7ffc1a901eea -r 052399f580cf src/HOL/NewNumberTheory/Residues.thy
--- a/src/HOL/NewNumberTheory/Residues.thy	Sat Jun 20 14:00:36 2009 +0200
+++ b/src/HOL/NewNumberTheory/Residues.thy	Sun Jun 21 11:50:26 2009 +0200
@@ -397,13 +397,13 @@
   shows "[fact (p - 1) = - 1] (mod p)"
 proof -
   let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}" 
-  have "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
+  have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
     by auto
-  hence "(\<Otimes>i: Units R. i) = 
+  have "(\<Otimes>i: Units R. i) = 
     (\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)"
-    apply (elim ssubst) back back
+    apply (subst UR)
     apply (subst finprod_Un_disjoint)
-    apply (auto intro!: funcsetI)
+    apply (auto intro:funcsetI)
     apply (drule sym, subst (asm) inv_eq_one_eq)
     apply auto
     apply (drule sym, subst (asm) inv_eq_neg_one_eq)
@@ -414,7 +414,6 @@
     apply auto
     apply (frule one_eq_neg_one)
     apply (insert a, force)
-    apply (auto intro!: funcsetI)
     done
   also have "(\<Otimes>i:(Union ?InversePairs). i) = 
       (\<Otimes> A: ?InversePairs. (\<Otimes> y:A. y))"
@@ -431,13 +430,13 @@
     apply (subst finprod_insert)
     apply auto
     apply (frule inv_eq_self)
-    apply (auto intro!: funcsetI)
+    apply (auto)
     done
   finally have "(\<Otimes>i: Units R. i) = \<ominus> \<one>"
     by simp
   also have "(\<Otimes>i: Units R. i) = (\<Otimes>i: Units R. i mod p)"
     apply (rule finprod_cong')
-    apply (auto intro!: funcsetI)
+    apply (auto)
     apply (subst (asm) res_prime_units_eq)
     apply auto
     done