Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Lattice/Orders.thy
changeset 40702 cf26dd7395e4
parent 39246 9e58f0499f57
child 56154 f0a927235162 
--- a/src/HOL/Lattice/Orders.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Lattice/Orders.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -118,8 +118,8 @@
   qed
 qed
 
-lemma range_dual [simp]: "dual ` UNIV = UNIV"
-proof (rule surj_range)
+lemma range_dual [simp]: "surj dual"
+proof -
   have "\<And>x'. dual (undual x') = x'" by simp
   thus "surj dual" by (rule surjI)
 qed
isabelle