# HG changeset patch
# User paulson
# Date 939631758 -7200
# Node ID 09aabe6d04b8d8499f38d6759f13590cf3f205f9
# Parent  a8717f53036cd0a136de9de4dbabd07ffa1f293e
new thm Domain_mono

diff -r a8717f53036c -r 09aabe6d04b8 src/HOL/Relation.ML
--- 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 **)