# HG changeset patch
# User krauss
# Date 1164372291 -3600
# Node ID 3786eb1b69d647da34047d84370e31d57fed6e43
# Parent  16c62deb1adfac23edfa0b5c99835e3cffdeb0b3
Lemma "fundef_default_value" uses predicate instead of set.

diff -r 16c62deb1adf -r 3786eb1b69d6 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Fri Nov 24 13:43:44 2006 +0100
+++ b/src/HOL/FunDef.thy	Fri Nov 24 13:44:51 2006 +0100
@@ -149,14 +149,15 @@
 
 lemma fundef_default_value:
 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
-assumes graph: "\<And>x y. G x y \<Longrightarrow> x \<in> D"
-assumes "x \<notin> D"
+assumes graph: "\<And>x y. G x y \<Longrightarrow> D x"
+assumes "\<not> D x"
 shows "f x = d x"
 proof -
   have "\<not>(\<exists>y. G x y)"
   proof
-    assume "(\<exists>y. G x y)"
-    with graph and `x\<notin>D` show False by blast
+    assume "\<exists>y. G x y"
+    hence "D x" using graph ..
+    with `\<not> D x` show False ..
   qed
   hence "\<not>(\<exists>!y. G x y)" by blast