# HG changeset patch
# User haftmann
# Date 1325933153 -3600
# Node ID 913ea585efdca0b589e8fb30b84288a6ba4a27f9
# Parent  d6cafcc012ec541e578e83f95df27c17dd8ca453
corrected slip

diff -r d6cafcc012ec -r 913ea585efdc src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Jan 07 09:32:18 2012 +0100
+++ b/src/HOL/List.thy	Sat Jan 07 11:45:53 2012 +0100
@@ -5216,10 +5216,10 @@
   by (simp add: member_def)
 
 definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
-  [code_abbrev]: list_all_iff: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
+  list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
 
 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
-  [code_abbrev]: list_ex_iff: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
+  list_ex_iff [code_abbrev]: "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)"