| changeset 4760 | 9cdbd5a1d25a |
| parent 4746 | a5dcd7e4a37d |
| child 4830 | bd73675adbed |
--- 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]);