list_all2_mono should not be [trans]
authorkleing
Tue Dec 23 23:40:16 2003 +0100 (2003-12-23)
changeset 143279cd4dea593e3
parent 14326 c817dd885a32
child 14328 fd063037fdf5
list_all2_mono should not be [trans]
src/HOL/List.thy
     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)