new theorem trans_O_subset

--- a/src/HOL/Relation.ML	Fri Jun 23 10:34:51 2000 +0200
+++ b/src/HOL/Relation.ML	Fri Jun 23 10:43:43 2000 +0200
@@ -111,6 +111,10 @@
 by (Blast_tac 1);
 qed "O_assoc";
 
+Goalw [trans_def] "trans r ==> r O r <= r";
+by (Blast_tac 1);
+qed "trans_O_subset";
+
 Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
 by (Blast_tac 1);
 qed "comp_mono";