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