src/HOL/Hyperreal/NatStar.thy
changeset 23719 ccd9cb15c062
parent 21865 55cc354fd2d9
child 26806 40b411ec05aa