changeset 60679 | ade12ef2773c |
parent 59581 | 09722854b8f4 |
child 60919 | b0ba7799d05a |
--- a/src/HOL/Library/DAList.thy Mon Jul 06 22:06:02 2015 +0200 +++ b/src/HOL/Library/DAList.thy Mon Jul 06 22:57:34 2015 +0200 @@ -93,7 +93,7 @@ definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys" instance - by default (simp add: equal_alist_def impl_of_inject) + by standard (simp add: equal_alist_def impl_of_inject) end