--- a/src/HOL/Library/Sublist_Order.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Sublist_Order.thy Fri Oct 10 06:45:53 2008 +0200
@@ -47,7 +47,7 @@
using assms by (induct rule: less_eq_list.induct) blast+
definition
- [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
+ [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
by (induct rule: ileq_induct) auto