src/HOL/Hyperreal/StarDef.thy
changeset 19459 2041d472fc17
parent 18708 4b3dadb4fe33
child 19765 dfe940911617