diff -r 76d9575950f2 -r 190974c664a3 src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Fri Dec 23 16:27:45 1994 +0100
+++ b/src/ZF/Perm.ML	Fri Dec 23 16:28:26 1994 +0100
@@ -63,6 +63,10 @@
 by (fast_tac ZF_cs 1);
 qed "inj_equality";
 
+goalw thy [inj_def] "!!A B f. [| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b";
+by (fast_tac ZF_cs 1);
+val inj_apply_equality = result();
+
 (** A function with a left inverse is an injection **)
 
 val prems = goal Perm.thy
@@ -122,6 +126,10 @@
 by (assume_tac 1);
 qed "id_type";
 
+goalw Perm.thy [id_def] "!!A x. x:A ==> id(A)`x = x";
+by (asm_simp_tac ZF_ss 1);
+val id_conv = result();
+
 val [prem] = goalw Perm.thy [id_def] "A<=B ==> id(A) <= id(B)";
 by (rtac (prem RS lam_mono) 1);
 qed "id_mono";