src/HOL/Hyperreal/StarClasses.thy
changeset 25600 73431bd8c4c4
parent 25571 c9e39eafc7a0