src/HOL/Relation.ML
changeset 4760 9cdbd5a1d25a
parent 4746 a5dcd7e4a37d
child 4830 bd73675adbed
     1.1 --- a/src/HOL/Relation.ML	Mon Mar 30 21:04:41 1998 +0200
     1.2 +++ b/src/HOL/Relation.ML	Mon Mar 30 21:05:25 1998 +0200
     1.3 @@ -231,3 +231,12 @@
     1.4  goal thy "r^^B = (UN y: B. r^^{y})";
     1.5  by (Blast_tac 1);
     1.6  qed "Image_eq_UN";
     1.7 +
     1.8 +
     1.9 +section "Univalent";
    1.10 +
    1.11 +qed_goalw "UnivalentI" Relation.thy [Univalent_def] 
    1.12 +   "!!r. !x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> Univalent r" (K [atac 1]);
    1.13 +
    1.14 +qed_goalw "UnivalentD" Relation.thy [Univalent_def] 
    1.15 +	"!!r. [| Univalent r; (x,y):r; (x,z):r|] ==> y=z" (K [Auto_tac]);