# HG changeset patch
# User haftmann
# Date 1245591974 -7200
# Node ID 41788a3ffd6a70ca345a5a468a4bee9c48e13dd3
# Parent  052399f580cfe701625c16b8248aa61a9532c573# Parent  002da20f442e91b7654cf35080c7b717dfba253a
merged

diff -r 002da20f442e -r 41788a3ffd6a src/HOL/NewNumberTheory/Residues.thy
--- a/src/HOL/NewNumberTheory/Residues.thy	Sun Jun 21 15:45:57 2009 +0200
+++ b/src/HOL/NewNumberTheory/Residues.thy	Sun Jun 21 15:46:14 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