Modified proof of "(R^=)^* = R^*" to accommodate equalityI.

--- a/src/HOL/Trancl.ML	Fri May 24 11:46:40 1996 +0200
+++ b/src/HOL/Trancl.ML	Fri May 24 11:48:18 1996 +0200
@@ -125,12 +125,13 @@
 qed "rtrancl_subset";
 
 goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
-by (best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl,
-                           rtrancl_mono RS subsetD]) 1);
+by (best_tac (!claset addSIs [rtrancl_subset]
+                      addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
 qed "rtrancl_Un_rtrancl";
 
 goal Trancl.thy "(R^=)^* = R^*";
-by (fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1);
+by (fast_tac (!claset addSIs [rtrancl_refl,rtrancl_subset]
+                      addIs  [r_into_rtrancl]) 1);
 qed "rtrancl_reflcl";
 Addsimps [rtrancl_reflcl];