src/HOL/Library/Sublist.thy
changeset 52729 412c9e0381a1
parent 50516 ed6b40d15d1c
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/Library/Sublist.thy	Wed Jul 24 17:15:59 2013 +0200
     1.2 +++ b/src/HOL/Library/Sublist.thy	Thu Jul 25 08:57:16 2013 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  interpretation prefix_order: order prefixeq prefix
     1.5    by default (auto simp: prefixeq_def prefix_def)
     1.6  
     1.7 -interpretation prefix_bot: bot prefixeq prefix Nil
     1.8 +interpretation prefix_bot: order_bot Nil prefixeq prefix
     1.9    by default (simp add: prefixeq_def)
    1.10  
    1.11  lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"