src/HOL/Real/Hyperreal/Hyperreal.thy
changeset 10168 50be659d4222
parent 10094 22f201e9ec7a
child 10690 cd80241125b0