changeset 63171 | a0088f1c049d |
parent 63092 | a949b2a5f51d |
child 63331 | 247eac9758dd |
--- a/src/HOL/Conditionally_Complete_Lattices.thy Fri May 27 20:23:55 2016 +0200 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Fri May 27 23:35:13 2016 +0200 @@ -631,7 +631,7 @@ qed ultimately show ?thesis unfolding greaterThanAtMost_def greaterThanLessThan_def atLeastAtMost_def atLeastLessThan_def - by (elim exE disjE) auto + by (metis inf_bot_left inf_bot_right inf_top.left_neutral inf_top.right_neutral) qed lemma cSUP_eq_cINF_D: