--- a/src/HOL/Library/Order_Relation.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Library/Order_Relation.thy Wed May 07 10:57:19 2008 +0200
@@ -103,7 +103,7 @@
lemma subset_Image_Image_iff:
"\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
-apply(auto simp add:subset_def preorder_on_def refl_def Image_def)
+apply(auto simp add: subset_eq preorder_on_def refl_def Image_def)
apply metis
by(metis trans_def)