merged
authornipkow
Mon Mar 26 21:00:39 2012 +0200 (2012-03-26)
changeset 47132bef6bc52a32e
parent 47129 bd1679890503
parent 47131 af818dcdc709
child 47133 89b13238d7f2
merged
     1.1 --- a/src/HOL/List.thy	Mon Mar 26 20:11:27 2012 +0200
     1.2 +++ b/src/HOL/List.thy	Mon Mar 26 21:00:39 2012 +0200
     1.3 @@ -5354,9 +5354,9 @@
     1.4    "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
     1.5    by (simp add: list_all_iff)
     1.6  
     1.7 -lemma list_any_cong [fundef_cong]:
     1.8 +lemma list_ex_cong [fundef_cong]:
     1.9    "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
    1.10 -  by (simp add: list_ex_iff)
    1.11 +by (simp add: list_ex_iff)
    1.12  
    1.13  text {* Executable checks for relations on sets *}
    1.14