src/HOL/Algebra/FiniteProduct.thy
changeset 23350 50c5b0912a0c
parent 22265 3c5c6bdf61de
child 23746 a455e69c31cc
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Wed Jun 13 00:01:38 2007 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Wed Jun 13 00:01:41 2007 +0200
     1.3 @@ -263,9 +263,9 @@
     1.4  
     1.5  lemma (in ACeD) left_ident [simp]: "x \<in> D ==> e \<cdot> x = x"
     1.6  proof -
     1.7 -  assume D: "x \<in> D"
     1.8 -  have "x \<cdot> e = x" by (rule ident)
     1.9 -  with D show ?thesis by (simp add: commute)
    1.10 +  assume "x \<in> D"
    1.11 +  then have "x \<cdot> e = x" by (rule ident)
    1.12 +  with `x \<in> D` show ?thesis by (simp add: commute)
    1.13  qed
    1.14  
    1.15  lemma (in ACeD) foldD_Un_Int:
    1.16 @@ -424,9 +424,9 @@
    1.17        then have "finprod G f A = finprod G f (insert x B)" by simp
    1.18        also from insert have "... = f x \<otimes> finprod G f B"
    1.19        proof (intro finprod_insert)
    1.20 -	show "finite B" .
    1.21 +	show "finite B" by fact
    1.22        next
    1.23 -	show "x ~: B" .
    1.24 +	show "x ~: B" by fact
    1.25        next
    1.26  	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
    1.27  	  "g \<in> insert x B \<rightarrow> carrier G"