--- a/src/HOL/Relation_Power.ML Fri Jan 05 18:33:47 2001 +0100
+++ b/src/HOL/Relation_Power.ML Fri Jan 05 18:48:18 2001 +0100
@@ -103,12 +103,12 @@
qed "rtrancl_is_UN_rel_pow";
-Goal "!!r::('a * 'a)set. univalent r ==> univalent (r^n)";
-by (rtac univalentI 1);
+Goal "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)";
+by (rtac single_valuedI 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";
+by (fast_tac (claset() addDs [single_valuedD] addEs [rel_pow_Suc_E]) 1);
+qed_spec_mp "single_valued_rel_pow";