src/HOL/Hyperreal/Hyperreal.thy
changeset 12378 86c58273f8c0
parent 12224 02df7cbe7d25
child 13958 c1c67582c9b5