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.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"