src/HOL/Hyperreal/StarDef.thy
changeset 20830 65ba80cae6df
parent 20719 bf00c5935432
child 21404 eb85850d3eb7