# HG changeset patch
# User haftmann
# Date 1224863316 -7200
# Node ID 48faac3240617b7097080a36a72d7a1f7118a605
# Parent  59c01ec6cb8d9d75040e8d52a5dbac1154d6c175
tuned proof

diff -r 59c01ec6cb8d -r 48faac324061 src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Fri Oct 24 17:48:35 2008 +0200
+++ b/src/HOL/Library/Enum.thy	Fri Oct 24 17:48:36 2008 +0200
@@ -53,7 +53,7 @@
   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 less_fun_def order_less_le)
+  by (simp_all add: list_all_iff enum_all expand_fun_eq le_fun_def order_less_le)
 
 
 subsection {* Quantifiers *}