src/HOL/Library/Prefix_Order.thy
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