--- a/src/HOL/Enum.thy Fri Dec 03 00:36:01 2010 +0100
+++ b/src/HOL/Enum.thy Fri Dec 03 08:40:46 2010 +0100
@@ -46,14 +46,14 @@
end
+lemma [code]:
+ "HOL.equal f g \<longleftrightarrow> list_all (%x. f x = g x) enum"
+by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
+
lemma [code nbe]:
"HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
by (fact equal_refl)
-lemma [code]:
- "HOL.equal f g \<longleftrightarrow> list_all (%x. f x = g x) enum"
-by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
-
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"