# HG changeset patch
# User haftmann
# Date 1310402698 -7200
# Node ID 366d5726de0962dbc3ba44f2c5e33a76263560b0
# Parent  52310132063bc6c4cf48d592e7a43c3f14611c70
explicit code equation for equality

diff -r 52310132063b -r 366d5726de09 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Mon Jul 11 17:22:31 2011 +0200
+++ b/src/HOL/Library/Dlist.thy	Mon Jul 11 18:44:58 2011 +0200
@@ -125,6 +125,8 @@
 
 end
 
+declare equal_dlist_def [code]
+
 lemma [code nbe]:
   "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
   by (fact equal_refl)