changed order of lemmas to overwrite the general code equation with the nbe-specific one
authorbulwahn
Fri Dec 03 08:40:46 2010 +0100 (2010-12-03)
changeset 40898882e860a1e83
parent 40897 1eb1b2f9d062
child 40899 ef6fde932f4c
changed order of lemmas to overwrite the general code equation with the nbe-specific one
src/HOL/Enum.thy
     1.1 --- a/src/HOL/Enum.thy	Fri Dec 03 00:36:01 2010 +0100
     1.2 +++ b/src/HOL/Enum.thy	Fri Dec 03 08:40:46 2010 +0100
     1.3 @@ -46,14 +46,14 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma [code]:
     1.8 +  "HOL.equal f g \<longleftrightarrow>  list_all (%x. f x = g x) enum"
     1.9 +by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
    1.10 +
    1.11  lemma [code nbe]:
    1.12    "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
    1.13    by (fact equal_refl)
    1.14  
    1.15 -lemma [code]:
    1.16 -  "HOL.equal f g \<longleftrightarrow>  list_all (%x. f x = g x) enum"
    1.17 -by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
    1.18 -
    1.19  lemma order_fun [code]:
    1.20    fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
    1.21    shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"