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"