Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid duplicate fact name
authorkleing
Fri, 18 Jul 2014 22:16:03 +0200
changeset 57573 2bfbeb0e69cd
parent 57572 57932dd40916
child 57574 e4ddd52e1b96
avoid duplicate fact name
src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy file | annotate | diff | comparison | revisions 
--- 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) \<squnion> \<bottom> = \<bottom>"
   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) \<squnion> \<bottom> = x"
   quickcheck[expect = no_counterexample]
   by (rule sup_absorb1) simp
isabelle