summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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