1.1 --- a/src/HOL/SetInterval.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -657,7 +657,7 @@
     1.4      case (insert b A)
     1.5      moreover hence "b ~: A" by auto
     1.6      moreover have "A <= {k..<k+card A}" and "b = k+card A"
     1.7 -      using `b ~: A` insert by fastsimp+
     1.8 +      using `b ~: A` insert by fastforce+
     1.9      ultimately show ?case by auto
    1.10    qed
    1.11  next
    1.12 @@ -688,7 +688,7 @@
    1.13  lemma UN_le_add_shift:
    1.14    "(\<Union>i\<le>n::nat. M(i+k)) = (\<Union>i\<in>{k..n+k}. M i)" (is "?A = ?B")
    1.15  proof
    1.16 -  show "?A <= ?B" by fastsimp
    1.17 +  show "?A <= ?B" by fastforce
    1.18  next
    1.19    show "?B <= ?A"
    1.20    proof
    1.21 @@ -899,7 +899,7 @@
    1.22  lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
    1.23  apply (rule card_bij_eq [of Suc _ _ "\<lambda>x. x - Suc 0"])
    1.24  apply simp
    1.25 -apply fastsimp
    1.26 +apply fastforce
    1.27  apply auto
    1.28  apply (rule inj_on_diff_nat)
    1.29  apply auto
    1.30 @@ -1020,7 +1020,7 @@
    1.31  apply(rule ccontr)
    1.32  apply(insert linorder_le_less_linear[of i n])
    1.33  apply(clarsimp simp:linorder_not_le)
    1.34 -apply(fastsimp)
    1.35 +apply(fastforce)
    1.36  done
    1.37  
    1.38