diff -r 470b579f35d2 -r 412c9e0381a1 src/HOL/Library/Sublist.thy --- a/src/HOL/Library/Sublist.thy Wed Jul 24 17:15:59 2013 +0200 +++ b/src/HOL/Library/Sublist.thy Thu Jul 25 08:57:16 2013 +0200 @@ -20,7 +20,7 @@ interpretation prefix_order: order prefixeq prefix by default (auto simp: prefixeq_def prefix_def) -interpretation prefix_bot: bot prefixeq prefix Nil +interpretation prefix_bot: order_bot Nil prefixeq prefix by default (simp add: prefixeq_def) lemma prefixeqI [intro?]: "ys = xs @ zs \ prefixeq xs ys"