# HG changeset patch
# User oheimb
# Date 891284681 -7200
# Node ID 33a03e70e6410cbc0aba15c26e89a4d79cff4b09
# Parent  35f4ad4f055dcb2eb4cc714f29ce495e157f6e46
added Univalent_rel_pow

diff -r 35f4ad4f055d -r 33a03e70e641 src/HOL/RelPow.ML
--- 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";
 
+
+
+