src/HOL/Hyperreal/Hyperreal.thy
changeset 12597 14822e4436bf
parent 12224 02df7cbe7d25
child 13958 c1c67582c9b5