# HG changeset patch
# User paulson
# Date 961749823 -7200
# Node ID e221d4f81d52e4c8d0dc93e8b03af9c352e2930e
# Parent  44fc37919579feddee2ca927f4a87dc4f9f9c7f9
new theorem trans_O_subset

diff -r 44fc37919579 -r e221d4f81d52 src/HOL/Relation.ML
--- 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";