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)"