| changeset 4830 | bd73675adbed |
| parent 4799 | 82b0ed20c2cb |
| child 4838 | 196100237656 |
--- a/src/HOL/Trancl.ML Mon Apr 27 13:47:46 1998 +0200 +++ b/src/HOL/Trancl.ML Mon Apr 27 16:45:11 1998 +0200 @@ -115,6 +115,13 @@ qed "rtrancl_idemp"; Addsimps [rtrancl_idemp]; +goal thy "R^* O R^* = R^*"; +br set_ext 1; +by(split_all_tac 1); +by(blast_tac (claset() addIs [rtrancl_trans]) 1); +qed "rtrancl_idemp_self_comp"; +Addsimps [rtrancl_idemp_self_comp]; + goal Trancl.thy "!!r s. r <= s^* ==> r^* <= s^*"; by (dtac rtrancl_mono 1); by (Asm_full_simp_tac 1);