# HG changeset patch
# User haftmann
# Date 1325925121 -3600
# Node ID 54ca5b2775a882c6ca363231e6ef390e62e380f3
# Parent  04a8da7dcffc11373ab81ac46a05c88a8c3b873e
restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)

diff -r 04a8da7dcffc -r 54ca5b2775a8 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jan 06 22:16:25 2012 +0100
+++ b/src/HOL/List.thy	Sat Jan 07 09:32:01 2012 +0100
@@ -5199,7 +5199,7 @@
 subsubsection {* Counterparts for set-related operations *}
 
 definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
-  "member xs x \<longleftrightarrow> x \<in> set xs"
+  [code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"
 
 text {*
   Use @{text member} only for generating executable code.  Otherwise use
@@ -5216,10 +5216,10 @@
   by (simp add: member_def)
 
 definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
-  list_all_iff: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
+  [code_abbrev]: list_all_iff: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
 
 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
-  list_ex_iff: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
+  [code_abbrev]: list_ex_iff: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
 
 definition list_ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
   list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"