new thm Domain_mono
authorpaulson
Mon Oct 11 10:49:18 1999 +0200 (1999-10-11)
changeset 782209aabe6d04b8
parent 7821 a8717f53036c
child 7823 742715638a01
new thm Domain_mono
src/HOL/Relation.ML
     1.1 --- a/src/HOL/Relation.ML	Mon Oct 11 10:48:44 1999 +0200
     1.2 +++ b/src/HOL/Relation.ML	Mon Oct 11 10:49:18 1999 +0200
     1.3 @@ -255,6 +255,10 @@
     1.4  by (Blast_tac 1);
     1.5  qed "Domain_Union";
     1.6  
     1.7 +Goal "r <= s ==> Domain r <= Domain s";
     1.8 +by (Blast_tac 1);
     1.9 +qed "Domain_mono";
    1.10 +
    1.11  
    1.12  (** Range **)
    1.13