src/HOL/Hyperreal/StarClasses.thy
changeset 23512 770e7f9f715b
parent 23282 dfc459989d24
child 23551 84f0996a530b