src/HOL/Relation.ML
changeset 7822 09aabe6d04b8
parent 7083 9663eb2bce05
child 7913 86be2946bb0b
equal deleted inserted replaced
7821:a8717f53036c 7822:09aabe6d04b8
   252 qed "Domain_Diff_subset";
   252 qed "Domain_Diff_subset";
   253 
   253 
   254 Goal "Domain (Union S) = (UN A:S. Domain A)";
   254 Goal "Domain (Union S) = (UN A:S. Domain A)";
   255 by (Blast_tac 1);
   255 by (Blast_tac 1);
   256 qed "Domain_Union";
   256 qed "Domain_Union";
       
   257 
       
   258 Goal "r <= s ==> Domain r <= Domain s";
       
   259 by (Blast_tac 1);
       
   260 qed "Domain_mono";
   257 
   261 
   258 
   262 
   259 (** Range **)
   263 (** Range **)
   260 
   264 
   261 Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)";
   265 Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)";