src/HOL/Complex/CStar.thy
 changeset 17292 5c613b64bf0a parent 15234 ec91a90c604e child 17298 ad73fb6144cf
equal inserted replaced
17291:94f6113fe9ed 17292:5c613b64bf0a
`   184 lemma InternalCSets_starsetC_n [simp]: "( *sc* X) \<in> InternalCSets"`
`   184 lemma InternalCSets_starsetC_n [simp]: "( *sc* X) \<in> InternalCSets"`
`   185 by (auto simp add: InternalCSets_def starsetC_starsetC_n_eq)`
`   185 by (auto simp add: InternalCSets_def starsetC_starsetC_n_eq)`
`   186 `
`   186 `
`   187 lemma InternalCSets_UNIV_diff:`
`   187 lemma InternalCSets_UNIV_diff:`
`   188     "X \<in> InternalCSets ==> UNIV - X \<in> InternalCSets"`
`   188     "X \<in> InternalCSets ==> UNIV - X \<in> InternalCSets"`
`       `
`   189 apply (subgoal_tac "UNIV - X = - X")`
`   189 by (auto intro: InternalCSets_Compl)`
`   190 by (auto intro: InternalCSets_Compl)`
`   190 `
`   191 `
`   191 text{*Nonstandard extension of a set (defined using a constant sequence) as a special case of an internal set*}`
`   192 text{*Nonstandard extension of a set (defined using a constant sequence) as a special case of an internal set*}`
`   192 `
`   193 `
`   193 lemma starsetC_n_starsetC: "\<forall>n. (As n = A) ==> *scn* As = *sc* A"`
`   194 lemma starsetC_n_starsetC: "\<forall>n. (As n = A) ==> *scn* As = *sc* A"`