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_mono should not be [trans]
authorkleing
Tue, 23 Dec 2003 23:40:16 +0100
changeset 14327 9cd4dea593e3
parent 14326 c817dd885a32
child 14328 fd063037fdf5
list_all2_mono should not be [trans]
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/List.thy	Tue Dec 23 18:26:03 2003 +0100
+++ b/src/HOL/List.thy	Tue Dec 23 23:40:16 2003 +0100
@@ -1169,7 +1169,7 @@
   apply (case_tac n, simp, simp)
   done
 
-lemma list_all2_mono [trans, intro?]:
+lemma list_all2_mono [intro?]:
   "\<And>y. list_all2 P x y \<Longrightarrow> (\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> list_all2 Q x y"
   apply (induct x, simp)
   apply (case_tac y, auto)
isabelle