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

src/HOL/List.thy

changeset 47640 | 62bfba15b212 |

parent 47436 | d8fad618a67a |

child 47841 | 179b5e7c9803 |

1.1 --- a/src/HOL/List.thy Fri Apr 20 23:57:29 2012 +0200 1.2 +++ b/src/HOL/List.thy Sat Apr 21 06:49:04 2012 +0200 1.3 @@ -2261,7 +2261,8 @@ 1.4 [consumes 1, case_names Nil Cons, induct set: list_all2]: 1.5 assumes P: "list_all2 P xs ys" 1.6 assumes Nil: "R [] []" 1.7 - assumes Cons: "\<And>x xs y ys. \<lbrakk>P x y; R xs ys\<rbrakk> \<Longrightarrow> R (x # xs) (y # ys)" 1.8 + assumes Cons: "\<And>x xs y ys. 1.9 + \<lbrakk>P x y; list_all2 P xs ys; R xs ys\<rbrakk> \<Longrightarrow> R (x # xs) (y # ys)" 1.10 shows "R xs ys" 1.11 using P 1.12 by (induct xs arbitrary: ys) (auto simp add: list_all2_Cons1 Nil Cons)