src/HOL/List.thy
changeset 14327 9cd4dea593e3
parent 14316 91b897b9a2dc
child 14328 fd063037fdf5
     1.1 --- a/src/HOL/List.thy	Tue Dec 23 18:26:03 2003 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Dec 23 23:40:16 2003 +0100
     1.3 @@ -1169,7 +1169,7 @@
     1.4    apply (case_tac n, simp, simp)
     1.5    done
     1.6  
     1.7 -lemma list_all2_mono [trans, intro?]:
     1.8 +lemma list_all2_mono [intro?]:
     1.9    "\<And>y. list_all2 P x y \<Longrightarrow> (\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> list_all2 Q x y"
    1.10    apply (induct x, simp)
    1.11    apply (case_tac y, auto)