src/HOL/Hyperreal/HSeries.thy
changeset 22172 e7d6cb237b5e
parent 21864 2ecfd8985982
child 22631 7ae5a6ab7bd6