new theorem update_type

--- a/src/ZF/Update.ML	Mon Dec 28 16:54:53 1998 +0100
+++ b/src/ZF/Update.ML	Mon Dec 28 16:56:07 1998 +0100
@@ -33,3 +33,9 @@
 qed "domain_update";
 Addsimps [domain_update];
 
+Goalw [update_def] "[| f: A -> B;  x : A;  y: B |] ==> f(x:=y) : A -> B";
+by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb, 
+				      apply_funtype, lam_type]) 1);
+qed "update_type";
+
+