src/HOL/List.thy
changeset 14328 fd063037fdf5
parent 14327 9cd4dea593e3
child 14338 a1add2de7601
     1.1 --- a/src/HOL/List.thy	Tue Dec 23 23:40:16 2003 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Dec 24 08:54:30 2003 +0100
     1.3 @@ -1125,7 +1125,7 @@
     1.4    "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
     1.5    by (simp add: list_all2_conv_all_nth)
     1.6  
     1.7 -lemma list_all2_nthD [intro?]:
     1.8 +lemma list_all2_nthD:
     1.9    "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
    1.10    by (simp add: list_all2_conv_all_nth)
    1.11