added Univalent_rel_pow

--- a/src/HOL/RelPow.ML	Mon Mar 30 21:04:13 1998 +0200
+++ b/src/HOL/RelPow.ML	Mon Mar 30 21:04:41 1998 +0200
@@ -106,4 +106,13 @@
 qed "rtrancl_is_UN_rel_pow";
 
 
+goal RelPow.thy "!!r::('a * 'a)set. Univalent r ==> Univalent (r^n)";
+by (rtac UnivalentI 1);
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (fast_tac (claset() addDs [UnivalentD] addEs [rel_pow_Suc_E]) 1);
+qed_spec_mp "Univalent_rel_pow";
 
+
+
+