src/HOL/Hyperreal/StarClasses.thy
changeset 20574 a10885a269cb
parent 20553 7ced6152e52c
child 20633 e98f59806244