src/HOL/Library/Sublist_Order.thy
changeset 28562 4e74209f113e
parent 27682 25aceefd4786
child 30738 0842e906300c
     1.1 --- a/src/HOL/Library/Sublist_Order.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Library/Sublist_Order.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4    using assms by (induct rule: less_eq_list.induct) blast+
     1.5  
     1.6  definition
     1.7 -  [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
     1.8 +  [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
     1.9  
    1.10  lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
    1.11    by (induct rule: ileq_induct) auto