--- a/src/HOL/Library/Dlist.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Dlist.thy Mon Jul 06 22:57:34 2015 +0200
@@ -120,15 +120,14 @@
definition "HOL.equal dxs dys \<longleftrightarrow> HOL.equal (list_of_dlist dxs) (list_of_dlist dys)"
-instance proof
-qed (simp add: equal_dlist_def equal list_of_dlist_inject)
+instance
+ by standard (simp add: equal_dlist_def equal list_of_dlist_inject)
end
declare equal_dlist_def [code]
-lemma [code nbe]:
- "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
+lemma [code nbe]: "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
by (fact equal_refl)