# HG changeset patch
# User wenzelm
# Date 1273237973 -7200
# Node ID bca8762be737e28a190c067ea5834dbcadfd4a13
# Parent  f5b63d2bd8fa056f02f6d9ba77740cdc581b828a# Parent  51e3b38a5e412b7d422bf6327c212e90d6f4a264
merged

diff -r 51e3b38a5e41 -r bca8762be737 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri May 07 14:47:09 2010 +0200
+++ b/src/HOL/Relation.thy	Fri May 07 15:12:53 2010 +0200
@@ -406,7 +406,7 @@
 lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s"
 by blast
 
-lemma fst_eq_Domain: "fst ` R = Domain R";
+lemma fst_eq_Domain: "fst ` R = Domain R"
 by (auto intro!:image_eqI)
 
 lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
@@ -457,7 +457,7 @@
 lemma Range_converse[simp]: "Range(r^-1) = Domain r"
 by blast
 
-lemma snd_eq_Range: "snd ` R = Range R";
+lemma snd_eq_Range: "snd ` R = Range R"
 by (auto intro!:image_eqI)
 
 
@@ -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