src/ZF/Update.ML
changeset 6048 88e6e55dd168
parent 5168 adafef6eb295
child 6068 2d8f3e1f1151
--- 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";
+
+