src/HOL/Hyperreal/NatStar.thy
changeset 21471 03a5ef1936c5
parent 21404 eb85850d3eb7
child 21847 59a68ed9f2f2
equal deleted inserted replaced
21470:7c1b59ddcd56 21471:03a5ef1936c5