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