src/HOL/Hyperreal/StarClasses.thy
changeset 24235 aea5c389a2f5
parent 24195 7d1a16c77f7c
child 24506 020db6ec334a