# HG changeset patch
# User paulson
# Date 900666823 -7200
# Node ID f23494fa8dc1c7ac6420a0988cf436c64c6f6c87
# Parent  21177b8a4d7f4a940a4daf2f719fa159c535fd33
A stronger apply_0, and new thm domain_lam

diff -r 21177b8a4d7f -r f23494fa8dc1 src/ZF/func.ML
--- a/src/ZF/func.ML	Fri Jul 17 10:50:28 1998 +0200
+++ b/src/ZF/func.ML	Fri Jul 17 11:13:43 1998 +0200
@@ -86,7 +86,7 @@
 
 (*Applying a function outside its domain yields 0*)
 goalw ZF.thy [apply_def]
-    "!!a b f. [| a ~: domain(f);  f: Pi(A,B) |] ==> f`a = 0";
+    "!!a. a ~: domain(f) ==> f`a = 0";
 by (rtac the_0 1);
 by (Blast_tac 1);
 qed "apply_0";
@@ -183,7 +183,11 @@
 by (Simp_tac 1);
 qed "lam_empty";
 
-Addsimps [beta, lam_empty];
+Goalw [lam_def] "domain(Lambda(A,b)) = A";
+by (Blast_tac 1);
+qed "domain_lam";
+
+Addsimps [beta, lam_empty, domain_lam];
 
 (*congruence rule for lambda abstraction*)
 val prems = goalw ZF.thy [lam_def]