src/HOL/Library/List_Prefix.thy
changeset 45236 ac4a2a66707d
parent 38857 97775f3e8722
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Fri Oct 21 14:06:15 2011 +0200
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Fri Oct 21 14:25:38 2011 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4  next
     1.5    assume "xs = ys @ [y] \<or> xs \<le> ys"
     1.6    then show "xs \<le> ys @ [y]"
     1.7 -    by (metis order_eq_iff strict_prefixE strict_prefixI' xt1(7))
     1.8 +    by (metis order_eq_iff order_trans prefixI)
     1.9  qed
    1.10  
    1.11  lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"