| changeset 20552 | 2c31dd358c21 |
| parent 20245 | 54db3583354f |
| child 20555 | 055d9a1bbddf |
--- a/src/HOL/Hyperreal/HyperDef.thy Sat Sep 16 02:35:58 2006 +0200 +++ b/src/HOL/Hyperreal/HyperDef.thy Sat Sep 16 02:40:00 2006 +0200 @@ -188,6 +188,9 @@ lemma inj_hypreal_of_real: "inj(hypreal_of_real)" by (rule inj_onI, simp) +lemma mem_Rep_star_iff: "(X \<in> Rep_star x) = (x = star_n X)" +by (cases x, simp add: star_n_def) + lemma Rep_star_star_n_iff [simp]: "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)" by (simp add: star_n_def)