src/HOL/Library/Sublist_Order.thy
changeset 37765 26bdfb7b680b
parent 33499 30e6e070bdb6
child 49084 e3973567ed4f
     1.1 --- a/src/HOL/Library/Sublist_Order.thy	Mon Jul 12 08:58:12 2010 +0200
     1.2 +++ b/src/HOL/Library/Sublist_Order.thy	Mon Jul 12 08:58:13 2010 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
     1.5  
     1.6  definition
     1.7 -  [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
     1.8 +  "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
     1.9  
    1.10  instance proof qed
    1.11