# HG changeset patch
# User paulson
# Date 914860567 -3600
# Node ID 88e6e55dd1682422381d179983fae140788f067c
# Parent  f2e0938ba38decae75ef9f8f0ee1715dad077264
new theorem update_type

diff -r f2e0938ba38d -r 88e6e55dd168 src/ZF/Update.ML
--- 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";
+
+