src/HOL/Hyperreal/Star.thy
changeset 20830 65ba80cae6df
parent 20732 275f9bd2ead9
child 21404 eb85850d3eb7