# HG changeset patch
# User nipkow
# Date 832931298 -7200
# Node ID 23922221ac875ead3de4fe354597641e85222bc9
# Parent  5db6b3ea0e286b8b92bcdb14e1425ad7ea976783
Modified proof of "(R^=)^* = R^*" to accommodate equalityI.

diff -r 5db6b3ea0e28 -r 23922221ac87 src/HOL/Trancl.ML
--- 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];