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 .