src/HOL/Library/Sublist.thy
changeset 52729 412c9e0381a1
parent 50516 ed6b40d15d1c
child 53015 a1119cf551e8
--- 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 \<Longrightarrow> prefixeq xs ys"