src/HOL/Algebra/FiniteProduct.thy
 changeset 44890 22f665a2e91c parent 41433 1b8ff770f02c child 46721 f88b187ad8ca
```     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sun Sep 11 22:56:05 2011 +0200
1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Sep 12 07:55:43 2011 +0200
1.3 @@ -171,7 +171,7 @@
1.4      (EX y. (A, y) \<in> foldSetD D f e & v = f x y)"
1.5    apply auto
1.6    apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
1.7 -     apply (fastsimp dest: foldSetD_imp_finite)
1.8 +     apply (fastforce dest: foldSetD_imp_finite)
1.9      apply assumption
1.10     apply assumption
1.11    apply (blast intro: foldSetD_determ)
1.12 @@ -328,7 +328,7 @@
1.13             apply fast
1.14            apply fast
1.15           apply assumption
1.16 -        apply (fastsimp intro: m_closed)
1.17 +        apply (fastforce intro: m_closed)
1.18         apply simp+
1.19     apply fast
1.20    apply (auto simp add: finprod_def)
1.21 @@ -431,13 +431,13 @@
1.22        next
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 \<in> B -> carrier G" by fastsimp
1.26 +        thus "f \<in> B -> carrier G" by fastforce
1.27        next
1.28          assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
1.29            "g \<in> insert x B \<rightarrow> carrier G"
1.30 -        thus "f x \<in> carrier G" by fastsimp
1.31 +        thus "f x \<in> carrier G" by fastforce
1.32        qed
1.33 -      also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
1.34 +      also from insert have "... = g x \<otimes> finprod G g B" by fastforce
1.35        also from insert have "... = finprod G g (insert x B)"
1.36        by (intro finprod_insert [THEN sym]) auto
1.37        finally show ?case .
```