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