1.1 --- a/src/HOL/List.thy	Thu Apr 10 17:48:33 2014 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Apr 10 17:48:54 2014 +0200
     1.3 @@ -6022,8 +6022,10 @@
     1.4    "x \<in> set xs \<longleftrightarrow> member xs x"
     1.5    by (simp add: member_def)
     1.6  
     1.7 -definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
     1.8 -list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
     1.9 +abbreviation "list_all == pred_list"
    1.10 +
    1.11 +lemma list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
    1.12 +unfolding pred_list_def ..
    1.13  
    1.14  definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.15  list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
    1.16 @@ -6037,7 +6039,7 @@
    1.17    and @{const list_ex1} in specifications.
    1.18  *}
    1.19  
    1.20 -lemma list_all_simps [simp, code]:
    1.21 +lemma list_all_simps [code]:
    1.22    "list_all P (x # xs) \<longleftrightarrow> P x \<and> list_all P xs"
    1.23    "list_all P [] \<longleftrightarrow> True"
    1.24    by (simp_all add: list_all_iff)