--- a/src/HOL/Library/Enum.thy Mon Jun 28 15:32:24 2010 +0200
+++ b/src/HOL/Library/Enum.thy Mon Jun 28 15:32:24 2010 +0200
@@ -49,8 +49,8 @@
lemma order_fun [code]:
fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
- and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum"
- by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def order_less_le)
+ and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum"
+ by (simp_all add: list_all_iff list_ex_iff enum_all expand_fun_eq le_fun_def order_less_le)
subsection {* Quantifiers *}
@@ -58,8 +58,8 @@
lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
by (simp add: list_all_iff enum_all)
-lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
- by (simp add: list_all_iff enum_all)
+lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum"
+ by (simp add: list_ex_iff enum_all)
subsection {* Default instances *}