src/HOL/Library/List_Prefix.thy
changeset 26445 17223cf843d8
parent 25764 878c37886eed
child 27368 9f90ac19e32b
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Thu Mar 27 19:04:38 2008 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu Mar 27 19:04:39 2008 +0100
     1.3 @@ -355,15 +355,15 @@
     1.4    shows "xs \<parallel> ys"
     1.5    using len neq
     1.6  proof (induct rule: list_induct2)
     1.7 -  case 1
     1.8 +  case Nil
     1.9    then show ?case by simp
    1.10  next
    1.11 -  case (2 a as b bs)
    1.12 +  case (Cons a as b bs)
    1.13    have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" by fact
    1.14    show ?case
    1.15    proof (cases "a = b")
    1.16      case True
    1.17 -    then have "as \<noteq> bs" using 2 by simp
    1.18 +    then have "as \<noteq> bs" using Cons by simp
    1.19      then show ?thesis by (rule Cons_parallelI2 [OF True ih])
    1.20    next
    1.21      case False