| changeset 60679 | ade12ef2773c |
| parent 60500 | 903bb1495239 |
| child 61337 | 4645502c3c64 |
--- a/src/HOL/Library/Prefix_Order.thy Mon Jul 06 22:06:02 2015 +0200 +++ b/src/HOL/Library/Prefix_Order.thy Mon Jul 06 22:57:34 2015 +0200 @@ -14,7 +14,8 @@ definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys" definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)" -instance by (default, unfold less_eq_list_def less_list_def) auto +instance + by standard (auto simp: less_eq_list_def less_list_def) end