# HG changeset patch
# User oheimb
# Date 951137827 -3600
# Node ID 722074b93cddb958d386a8551d5fd5a4ffd2d89c
# Parent  2ae7f9b2c0bf6cee8d27a35d80de5266670319dc
renamed Univalent to univalent

diff -r 2ae7f9b2c0bf -r 722074b93cdd src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Mon Feb 21 11:16:19 2000 +0100
+++ b/src/HOL/RelPow.ML	Mon Feb 21 13:57:07 2000 +0100
@@ -105,12 +105,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. 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";
+by (fast_tac (claset() addDs [univalentD] addEs [rel_pow_Suc_E]) 1);
+qed_spec_mp "univalent_rel_pow";
 
 
 
diff -r 2ae7f9b2c0bf -r 722074b93cdd src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Mon Feb 21 11:16:19 2000 +0100
+++ b/src/HOL/Relation.ML	Mon Feb 21 13:57:07 2000 +0100
@@ -398,17 +398,17 @@
 by (Blast_tac 1);
 qed "Image_subset_eq";
 
-section "Univalent";
+section "univalent";
 
-Goalw [Univalent_def]
-     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r";
+Goalw [univalent_def]
+     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> univalent r";
 by (assume_tac 1);
-qed "UnivalentI";
+qed "univalentI";
 
-Goalw [Univalent_def]
-     "[| Univalent r;  (x,y):r;  (x,z):r|] ==> y=z";
+Goalw [univalent_def]
+     "[| univalent r;  (x,y):r;  (x,z):r|] ==> y=z";
 by Auto_tac;
-qed "UnivalentD";
+qed "univalentD";
 
 
 (** Graphs of partial functions **)
diff -r 2ae7f9b2c0bf -r 722074b93cdd src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Feb 21 11:16:19 2000 +0100
+++ b/src/HOL/Relation.thy	Mon Feb 21 13:57:07 2000 +0100
@@ -40,8 +40,8 @@
   trans  :: "('a * 'a)set => bool"          (*transitivity predicate*)
     "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
 
-  Univalent :: "('a * 'b)set => bool"
-    "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
+  univalent :: "('a * 'b)set => bool"
+    "univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
 
   fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
     "fun_rel_comp f R == {g. !x. (f x, g x) : R}"