src/HOL/Hyperreal/StarDef.thy
changeset 18960 9881ff995ff5
parent 18708 4b3dadb4fe33
child 19765 dfe940911617