src/HOL/Hyperreal/Hyperreal.thy
changeset 25247 7bacd1798fc4
parent 22983 3314057c3b57
child 26121 d4fbf84a6636