src/HOL/Algebra/Lattice.thy

   fix s
   assume sup: "least L s (Upper L {x, y, z})"
   show "x \<squnion> (y \<squnion> z) .= s"
   proof (rule weak_le_antisym)
     from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
-      by (fastsimp intro!: join_le elim: least_Upper_above)
+      by (fastforce intro!: join_le elim: least_Upper_above)
   next
     from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
     by (erule_tac least_le)
       (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)
   qed (simp_all add: L least_closed [OF sup])

   fix i
   assume inf: "greatest L i (Lower L {x, y, z})"
   show "x \<sqinter> (y \<sqinter> z) .= i"
   proof (rule weak_le_antisym)
     from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
-      by (fastsimp intro!: meet_le elim: greatest_Lower_below)
+      by (fastforce intro!: meet_le elim: greatest_Lower_below)
   next
     from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
     by (erule_tac greatest_le)
       (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)
   qed (simp_all add: L greatest_closed [OF inf])

   fix B
   assume B: "B \<subseteq> carrier ?L"
   show "EX s. least ?L s (Upper ?L B)"
   proof
     from B show "least ?L (\<Union> B) (Upper ?L B)"
-      by (fastsimp intro!: least_UpperI simp: Upper_def)
+      by (fastforce intro!: least_UpperI simp: Upper_def)
   qed
 next
   fix B
   assume B: "B \<subseteq> carrier ?L"
   show "EX i. greatest ?L i (Lower ?L B)"
   proof
     from B show "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
       txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
         @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
-      by (fastsimp intro!: greatest_LowerI simp: Lower_def)
+      by (fastforce intro!: greatest_LowerI simp: Lower_def)
   qed
 qed
 
 text {* An other example, that of the lattice of subgroups of a group,
   can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}