src/ZF/Perm.ML

--- a/src/ZF/Perm.ML	Fri Aug 12 12:51:34 1994 +0200
+++ b/src/ZF/Perm.ML	Fri Aug 12 18:45:33 1994 +0200
@@ -135,6 +135,14 @@
 by (fast_tac (ZF_cs addIs [id_inj,id_surj]) 1);
 val id_bij = result();
 
+goalw Perm.thy [id_def] "A <= B <-> id(A) : A->B";
+by (safe_tac ZF_cs);
+by (fast_tac (ZF_cs addSIs [lam_type]) 1);
+by (dtac apply_type 1);
+by (assume_tac 1);
+by (asm_full_simp_tac ZF_ss 1);
+val subset_iff_id = result();
+
 
 (*** Converse of a function ***)