# HG changeset patch
# User haftmann
# Date 1277731944 -7200
# Node ID 2a4fb776ca53a6c393f049d0aafc665fe3b609f6
# Parent  18f69eb29e66b6f1ab5887f87ea853f3aab19edc
tuned lemma formulations

diff -r 18f69eb29e66 -r 2a4fb776ca53 src/HOL/Library/Enum.thy
--- 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 *}