# HG changeset patch
# User haftmann
# Date 1553282289 0
# Node ID 77a92e8d5167af85a69f5909b8d4285b1010b847
# Parent  494934c30f382234aaff30bb0505f9e5db4e0fb3
executable equality

diff -r 494934c30f38 -r 77a92e8d5167 src/HOL/Library/Dual_Ordered_Lattice.thy
--- 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>