src/HOL/Hyperreal/Hyperreal.thy
changeset 12486 0ed8bdd883e0
parent 12224 02df7cbe7d25
child 13958 c1c67582c9b5