src/HOL/Hyperreal/StarClasses.thy
changeset 25322 e2eac0c30ff5
parent 25304 7491c00f0915
child 25571 c9e39eafc7a0