# HG changeset patch
# User oheimb
# Date 891284725 -7200
# Node ID 9cdbd5a1d25aa71ccefc0d47daf61dd00dd6fb19
# Parent  33a03e70e6410cbc0aba15c26e89a4d79cff4b09
added introduction and elimination rules for Univalent

diff -r 33a03e70e641 -r 9cdbd5a1d25a src/HOL/Relation.ML
--- 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]);