--- a/src/HOL/Library/Sublist.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Sublist.thy Mon Jul 06 22:57:34 2015 +0200
@@ -18,10 +18,10 @@
where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
interpretation prefix_order: order prefixeq prefix
- by default (auto simp: prefixeq_def prefix_def)
+ by standard (auto simp: prefixeq_def prefix_def)
interpretation prefix_bot: order_bot Nil prefixeq prefix
- by default (simp add: prefixeq_def)
+ by standard (simp add: prefixeq_def)
lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
unfolding prefixeq_def by blast