restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)
authorhaftmann
Sat Jan 07 09:32:01 2012 +0100 (2012-01-07)
changeset 4614954ca5b2775a8
parent 46148 04a8da7dcffc
child 46150 d6cafcc012ec
restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Fri Jan 06 22:16:25 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Jan 07 09:32:01 2012 +0100
     1.3 @@ -5199,7 +5199,7 @@
     1.4  subsubsection {* Counterparts for set-related operations *}
     1.5  
     1.6  definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
     1.7 -  "member xs x \<longleftrightarrow> x \<in> set xs"
     1.8 +  [code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"
     1.9  
    1.10  text {*
    1.11    Use @{text member} only for generating executable code.  Otherwise use
    1.12 @@ -5216,10 +5216,10 @@
    1.13    by (simp add: member_def)
    1.14  
    1.15  definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.16 -  list_all_iff: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
    1.17 +  [code_abbrev]: list_all_iff: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
    1.18  
    1.19  definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.20 -  list_ex_iff: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
    1.21 +  [code_abbrev]: list_ex_iff: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
    1.22  
    1.23  definition list_ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.24    list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"