added introduction and elimination rules for Univalent

--- a/src/HOL/Relation.ML	Mon Mar 30 21:04:41 1998 +0200
+++ b/src/HOL/Relation.ML	Mon Mar 30 21:05:25 1998 +0200
@@ -231,3 +231,12 @@
 goal thy "r^^B = (UN y: B. r^^{y})";
 by (Blast_tac 1);
 qed "Image_eq_UN";
+
+
+section "Univalent";
+
+qed_goalw "UnivalentI" Relation.thy [Univalent_def] 
+   "!!r. !x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r" (K [atac 1]);
+
+qed_goalw "UnivalentD" Relation.thy [Univalent_def] 
+	"!!r. [| Univalent r; (x,y):r; (x,z):r|] ==> y=z" (K [Auto_tac]);