slightly more robust proof
authorkrauss
Tue Oct 12 21:30:44 2010 +0200 (2010-10-12)
changeset 399909b4341366b63
parent 39989 ad60d7311f43
child 39991 8a2c75478357
slightly more robust proof
src/HOL/Algebra/Lattice.thy
     1.1 --- a/src/HOL/Algebra/Lattice.thy	Mon Oct 11 08:32:09 2010 -0700
     1.2 +++ b/src/HOL/Algebra/Lattice.thy	Tue Oct 12 21:30:44 2010 +0200
     1.3 @@ -233,9 +233,8 @@
     1.4    assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
     1.5      and AA': "A {.=} A'"
     1.6    shows "Lower L A = Lower L A'"
     1.7 -using Lower_memD[of y]
     1.8  unfolding Lower_def
     1.9 -apply safe
    1.10 +apply rule
    1.11   apply clarsimp defer 1
    1.12   apply clarsimp defer 1
    1.13  proof -