src/HOL/Hyperreal/NatStar.thy
changeset 14494 48ae8d678d88
parent 14468 6be497cacab5
child 14641 79b7bd936264