# 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 \ True" by (fact equal_refl)