# HG changeset patch
# User kuncar
# Date 1397144934 -7200
# Node ID 907f04603177ebf4c493b2ffcafe137f714ba807
# Parent  58ac520db7aef40b1c350164b8921b5254c5678e
make list_all an abbreviation of pred_list - prevent duplication

diff -r 58ac520db7ae -r 907f04603177 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Apr 10 17:48:33 2014 +0200
+++ b/src/HOL/List.thy	Thu Apr 10 17:48:54 2014 +0200
@@ -6022,8 +6022,10 @@
   "x \<in> set xs \<longleftrightarrow> member xs x"
   by (simp add: member_def)
 
-definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
-list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
+abbreviation "list_all == pred_list"
+
+lemma list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
+unfolding pred_list_def ..
 
 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
 list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
@@ -6037,7 +6039,7 @@
   and @{const list_ex1} in specifications.
 *}
 
-lemma list_all_simps [simp, code]:
+lemma list_all_simps [code]:
   "list_all P (x # xs) \<longleftrightarrow> P x \<and> list_all P xs"
   "list_all P [] \<longleftrightarrow> True"
   by (simp_all add: list_all_iff)