# HG changeset patch
# User huffman
# Date 1334983744 -7200
# Node ID 62bfba15b212ed87cec685880df234d8666fa086
# Parent  2f7eb28c8b0989686b319ca22ea7b396d1e3b7ac
strengthen rule list_all2_induct

diff -r 2f7eb28c8b09 -r 62bfba15b212 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Apr 20 23:57:29 2012 +0200
+++ b/src/HOL/List.thy	Sat Apr 21 06:49:04 2012 +0200
@@ -2261,7 +2261,8 @@
   [consumes 1, case_names Nil Cons, induct set: list_all2]:
   assumes P: "list_all2 P xs ys"
   assumes Nil: "R [] []"
-  assumes Cons: "\<And>x xs y ys. \<lbrakk>P x y; R xs ys\<rbrakk> \<Longrightarrow> R (x # xs) (y # ys)"
+  assumes Cons: "\<And>x xs y ys.
+    \<lbrakk>P x y; list_all2 P xs ys; R xs ys\<rbrakk> \<Longrightarrow> R (x # xs) (y # ys)"
   shows "R xs ys"
 using P
 by (induct xs arbitrary: ys) (auto simp add: list_all2_Cons1 Nil Cons)