src/HOL/Algebra/Lattice.thy
 changeset 44890 22f665a2e91c parent 44655 fe0365331566 child 46008 c296c75f4cf4
```     1.1 --- a/src/HOL/Algebra/Lattice.thy	Sun Sep 11 22:56:05 2011 +0200
1.2 +++ b/src/HOL/Algebra/Lattice.thy	Mon Sep 12 07:55:43 2011 +0200
1.3 @@ -644,7 +644,7 @@
1.4    show "x \<squnion> (y \<squnion> z) .= s"
1.5    proof (rule weak_le_antisym)
1.6      from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
1.7 -      by (fastsimp intro!: join_le elim: least_Upper_above)
1.8 +      by (fastforce intro!: join_le elim: least_Upper_above)
1.9    next
1.10      from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
1.11      by (erule_tac least_le)
1.12 @@ -885,7 +885,7 @@
1.13    show "x \<sqinter> (y \<sqinter> z) .= i"
1.14    proof (rule weak_le_antisym)
1.15      from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
1.16 -      by (fastsimp intro!: meet_le elim: greatest_Lower_below)
1.17 +      by (fastforce intro!: meet_le elim: greatest_Lower_below)
1.18    next
1.19      from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
1.20      by (erule_tac greatest_le)
1.21 @@ -1289,7 +1289,7 @@
1.22    show "EX s. least ?L s (Upper ?L B)"
1.23    proof
1.24      from B show "least ?L (\<Union> B) (Upper ?L B)"
1.25 -      by (fastsimp intro!: least_UpperI simp: Upper_def)
1.26 +      by (fastforce intro!: least_UpperI simp: Upper_def)
1.27    qed
1.28  next
1.29    fix B
1.30 @@ -1299,7 +1299,7 @@
1.31      from B show "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
1.32        txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
1.33          @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
1.34 -      by (fastsimp intro!: greatest_LowerI simp: Lower_def)
1.35 +      by (fastforce intro!: greatest_LowerI simp: Lower_def)
1.36    qed
1.37  qed
1.38
```