diff -r 47ba1770da8e -r ae397b810c8b src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri May 07 09:59:59 2010 +0200
+++ b/src/HOL/Relation.thy	Fri May 07 15:03:53 2010 +0200
@@ -639,9 +639,16 @@
   done
 
 
-subsection {* Version of @{text lfp_induct} for binary relations *}
+subsection {* Miscellaneous *}
+
+text {* Version of @{thm[source] lfp_induct} for binary relations *}
 
 lemmas lfp_induct2 = 
   lfp_induct_set [of "(a, b)", split_format (complete)]
 
+text {* Version of @{thm[source] subsetI} for binary relations *}
+
+lemma subrelI: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (x, y) \<in> s) \<Longrightarrow> r \<subseteq> s"
+by auto
+
 end