| changeset 4830 | bd73675adbed |
| parent 4760 | 9cdbd5a1d25a |
| child 5069 | 3ea049f7979d |
--- a/src/HOL/Relation.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/Relation.ML Mon Apr 27 16:45:11 1998 +0200 @@ -64,6 +64,10 @@ Addsimps [R_O_id,id_O_R]; +goal thy "(R O S) O T = R O (S O T)"; +by (Blast_tac 1); +qed "O_assoc"; + goal thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"; by (Blast_tac 1); qed "comp_mono";