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)