# HG changeset patch # User kleing # Date 1405714563 -7200 # Node ID 2bfbeb0e69cd1a193ccca2e5ab0805dae75267f6 # Parent 57932dd40916319e9705e20cdb31abb814b686bc avoid duplicate fact name diff -r 57932dd40916 -r 2bfbeb0e69cd src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy --- a/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy Fri Jul 18 21:40:11 2014 +0200 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy Fri Jul 18 22:16:03 2014 +0200 @@ -84,7 +84,7 @@ quickcheck[expect = counterexample] oops -lemma inf_bot_right [simp]: +lemma sup_bot_right [simp]: "(x :: 'a :: bounded_lattice_bot) \ \ = \" quickcheck[expect = counterexample] oops @@ -94,7 +94,7 @@ quickcheck[expect = no_counterexample] by (rule sup_absorb2) simp -lemma sup_bot_right [simp]: +lemma sup_bot_right_2 [simp]: "(x :: 'a :: bounded_lattice_bot) \ \ = x" quickcheck[expect = no_counterexample] by (rule sup_absorb1) simp