--- a/src/HOL/Library/Dual_Ordered_Lattice.thy Fri Mar 22 19:18:08 2019 +0000
+++ b/src/HOL/Library/Dual_Ordered_Lattice.thy Fri Mar 22 19:18:09 2019 +0000
@@ -24,6 +24,8 @@
setup_lifting type_definition_dual
+code_datatype dual
+
lemma dual_eqI:
"x = y" if "undual x = undual y"
using that by transfer assumption
@@ -36,7 +38,7 @@
"dual x = dual y \<longleftrightarrow> x = y"
by transfer simp
-lemma undual_dual [simp]:
+lemma undual_dual [simp, code]:
"undual (dual x) = x"
by transfer rule
@@ -84,6 +86,17 @@
by (simp add: surj_dual)
qed
+instantiation dual :: (equal) equal
+begin
+
+lift_definition equal_dual :: "'a dual \<Rightarrow> 'a dual \<Rightarrow> bool"
+ is HOL.equal .
+
+instance
+ by (standard; transfer) (simp add: equal)
+
+end
+
subsection \<open>Pointwise ordering\<close>