src/HOL/Hyperreal/StarClasses.thy
changeset 23552 6403d06abe25
parent 23551 84f0996a530b
child 23879 4776af8be741