src/HOL/Enum.thy

 instance proof
 qed (simp_all add: equal_fun_def enum_all fun_eq_iff)
 
 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"
     and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum"