tuned proof
authorhaftmann
Fri Oct 24 17:48:36 2008 +0200 (2008-10-24)
changeset 2868448faac324061
parent 28683 59c01ec6cb8d
child 28685 275122631271
tuned proof
src/HOL/Library/Enum.thy
     1.1 --- a/src/HOL/Library/Enum.thy	Fri Oct 24 17:48:35 2008 +0200
     1.2 +++ b/src/HOL/Library/Enum.thy	Fri Oct 24 17:48:36 2008 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4    fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
     1.5    shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
     1.6      and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum"
     1.7 -  by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def less_fun_def order_less_le)
     1.8 +  by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def order_less_le)
     1.9  
    1.10  
    1.11  subsection {* Quantifiers *}