src/HOL/Hyperreal/Hyperreal.thy
changeset 12486 0ed8bdd883e0
parent 12224 02df7cbe7d25
child 13958 c1c67582c9b5
equal deleted inserted replaced
12485:3df60299a6d0 12486:0ed8bdd883e0