src/HOL/Algebra/FiniteProduct.thy
changeset 32960 69916a850301
parent 32693 6c6b1ba5e71e
child 35054 a5db9779b026
--- a/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -423,17 +423,17 @@
       then have "finprod G f A = finprod G f (insert x B)" by simp
       also from insert have "... = f x \<otimes> finprod G f B"
       proof (intro finprod_insert)
-	show "finite B" by fact
+        show "finite B" by fact
       next
-	show "x ~: B" by fact
+        show "x ~: B" by fact
       next
-	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
-	  "g \<in> insert x B \<rightarrow> carrier G"
-	thus "f \<in> B -> carrier G" by fastsimp
+        assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
+          "g \<in> insert x B \<rightarrow> carrier G"
+        thus "f \<in> B -> carrier G" by fastsimp
       next
-	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
-	  "g \<in> insert x B \<rightarrow> carrier G"
-	thus "f x \<in> carrier G" by fastsimp
+        assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
+          "g \<in> insert x B \<rightarrow> carrier G"
+        thus "f x \<in> carrier G" by fastsimp
       qed
       also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
       also from insert have "... = finprod G g (insert x B)"