--- a/src/HOL/Trancl.ML Sat May 13 13:46:48 1995 +0200
+++ b/src/HOL/Trancl.ML Sat May 13 14:08:24 1995 +0200
@@ -220,6 +220,23 @@
by (resolve_tac prems 1);
qed "trancl_into_trancl2";
+(*More about r^*)
+
+goal Trancl.thy "!!r. (b,c):r^* ==> !a. (a,b):r^* --> (a,c):r^*";
+be rtrancl_induct 1;
+by(ALLGOALS(fast_tac (comp_cs addIs [rtrancl_into_rtrancl])));
+bind_thm ("rtrancl_comp", result() RS spec RSN (2,rev_mp));
+
+goal Trancl.thy "(r^*)^* = r^*";
+br set_ext 1;
+by(res_inst_tac [("p","x")] PairE 1);
+by(hyp_subst_tac 1);
+br iffI 1;
+be rtrancl_induct 1;
+br rtrancl_refl 1;
+by(fast_tac (HOL_cs addEs [rtrancl_comp]) 1);
+be r_into_rtrancl 1;
+qed "rtrancl_idemp";
val major::prems = goal Trancl.thy
"[| (a,b) : r^*; r <= Sigma A (%x.A) |] ==> a=b | a:A";