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