--- a/src/HOL/Relation.ML Mon Oct 11 10:48:44 1999 +0200
+++ b/src/HOL/Relation.ML Mon Oct 11 10:49:18 1999 +0200
@@ -255,6 +255,10 @@
by (Blast_tac 1);
qed "Domain_Union";
+Goal "r <= s ==> Domain r <= Domain s";
+by (Blast_tac 1);
+qed "Domain_mono";
+
(** Range **)