src/ZF/OrdQuant.thy
 changeset 13149 773657d466cb parent 13118 336b0bcbd27c child 13162 660a71e712af
equal inserted replaced
13148:fe118a977a6d 13149:773657d466cb
`    82 `
`    82 `
`    83 lemma function_lam: "function (lam x:A. b(x))"`
`    83 lemma function_lam: "function (lam x:A. b(x))"`
`    84 by (simp add: function_def lam_def) `
`    84 by (simp add: function_def lam_def) `
`    85 `
`    85 `
`    86 lemma relation_lam: "relation (lam x:A. b(x))"  `
`    86 lemma relation_lam: "relation (lam x:A. b(x))"  `
`    87 by (simp add: relation_def lam_def, blast) `
`    87 by (simp add: relation_def lam_def) `
`    88 `
`    88 `
`    89 lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"`
`    89 lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"`
`    90 by (simp add: restrict_def) `
`    90 by (simp add: restrict_def) `
`    91 `
`    91 `
`    92 (** These mostly belong to theory Ordinal **)`
`    92 (** These mostly belong to theory Ordinal **)`