src/HOL/Library/FuncSet.thy
changeset 28524 644b62cf678f
parent 27487 c8a6ce181805
child 30663 0b6aff7451b2
     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Oct 07 16:07:40 2008 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Oct 07 16:07:50 2008 +0200
     1.3 @@ -15,11 +15,11 @@
     1.4  
     1.5  definition
     1.6    extensional :: "'a set => ('a => 'b) set" where
     1.7 -  "extensional A = {f. \<forall>x. x~:A --> f x = arbitrary}"
     1.8 +  "extensional A = {f. \<forall>x. x~:A --> f x = undefined}"
     1.9  
    1.10  definition
    1.11    "restrict" :: "['a => 'b, 'a set] => ('a => 'b)" where
    1.12 -  "restrict f A = (%x. if x \<in> A then f x else arbitrary)"
    1.13 +  "restrict f A = (%x. if x \<in> A then f x else undefined)"
    1.14  
    1.15  abbreviation
    1.16    funcset :: "['a set, 'b set] => ('a => 'b) set"
    1.17 @@ -117,7 +117,7 @@
    1.18    by (simp add: Pi_def restrict_def)
    1.19  
    1.20  lemma restrict_apply [simp]:
    1.21 -    "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)"
    1.22 +    "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)"
    1.23    by (simp add: restrict_def)
    1.24  
    1.25  lemma restrict_ext:
    1.26 @@ -164,7 +164,7 @@
    1.27  
    1.28  subsection{*Extensionality*}
    1.29  
    1.30 -lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary"
    1.31 +lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = undefined"
    1.32    by (simp add: extensional_def)
    1.33  
    1.34  lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"