src/HOL/Algebra/FiniteProduct.thy
 changeset 32960 69916a850301 parent 32693 6c6b1ba5e71e child 35054 a5db9779b026
```     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 17 01:05:59 2009 +0200
1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 17 14:43:18 2009 +0200
1.3 @@ -423,17 +423,17 @@
1.4        then have "finprod G f A = finprod G f (insert x B)" by simp
1.5        also from insert have "... = f x \<otimes> finprod G f B"
1.6        proof (intro finprod_insert)
1.7 -	show "finite B" by fact
1.8 +        show "finite B" by fact
1.9        next
1.10 -	show "x ~: B" by fact
1.11 +        show "x ~: B" by fact
1.12        next
1.13 -	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
1.14 -	  "g \<in> insert x B \<rightarrow> carrier G"
1.15 -	thus "f \<in> B -> carrier G" by fastsimp
1.16 +        assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
1.17 +          "g \<in> insert x B \<rightarrow> carrier G"
1.18 +        thus "f \<in> B -> carrier G" by fastsimp
1.19        next
1.20 -	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
1.21 -	  "g \<in> insert x B \<rightarrow> carrier G"
1.22 -	thus "f x \<in> carrier G" by fastsimp
1.23 +        assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
1.24 +          "g \<in> insert x B \<rightarrow> carrier G"
1.25 +        thus "f x \<in> carrier G" by fastsimp
1.26        qed
1.27        also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
1.28        also from insert have "... = finprod G g (insert x B)"
```