# HG changeset patch
# User krauss
# Date 1286911844 -7200
# Node ID 9b4341366b63af4d63ceb44f6bcb4d0a09319fa2
# Parent  ad60d7311f4360954f62b96e1e79aca591c9fa81
slightly more robust proof

diff -r ad60d7311f43 -r 9b4341366b63 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Mon Oct 11 08:32:09 2010 -0700
+++ b/src/HOL/Algebra/Lattice.thy	Tue Oct 12 21:30:44 2010 +0200
@@ -233,9 +233,8 @@
   assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
     and AA': "A {.=} A'"
   shows "Lower L A = Lower L A'"
-using Lower_memD[of y]
 unfolding Lower_def
-apply safe
+apply rule
  apply clarsimp defer 1
  apply clarsimp defer 1
 proof -