src/HOL/Nonstandard_Analysis/NatStar.thy
changeset 68975 5ce4d117cea7
parent 67399 eab6ce8368fa
child 69597 ff784d5a5bfb