# HG changeset patch
# User wenzelm
# Date 1310419240 -7200
# Node ID 24b8244d672bf6e4809f120b14ac49ca87787d1c
# Parent  366d5726de0962dbc3ba44f2c5e33a76263560b0# Parent  ab11dcfa3e6d3e4829425c39310a46b617616a9c
merged

diff -r ab11dcfa3e6d -r 24b8244d672b src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Mon Jul 11 23:15:27 2011 +0200
+++ b/src/HOL/Library/Dlist.thy	Mon Jul 11 23:20:40 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)