Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
list_all2_nthD no good as [intro?]
authorkleing
Wed, 24 Dec 2003 08:54:30 +0100
changeset 14328 fd063037fdf5
parent 14327 9cd4dea593e3
child 14329 ff3210fe968f
list_all2_nthD no good as [intro?]
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/List.thy	Tue Dec 23 23:40:16 2003 +0100
+++ b/src/HOL/List.thy	Wed Dec 24 08:54:30 2003 +0100
@@ -1125,7 +1125,7 @@
   "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
   by (simp add: list_all2_conv_all_nth)
 
-lemma list_all2_nthD [intro?]:
+lemma list_all2_nthD:
   "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
   by (simp add: list_all2_conv_all_nth)
isabelle