| changeset 21865 | 55cc354fd2d9 |
| parent 21864 | 2ecfd8985982 |
| child 26806 | 40b411ec05aa |
--- a/src/HOL/Hyperreal/NatStar.thy Sat Dec 16 19:37:07 2006 +0100 +++ b/src/HOL/Hyperreal/NatStar.thy Sat Dec 16 20:23:45 2006 +0100 @@ -8,7 +8,7 @@ header{*Star-transforms for the Hypernaturals*} theory NatStar -imports HyperPow +imports Star begin lemma star_n_eq_starfun_whn: "star_n X = ( *f* X) whn"