src/HOL/Nonstandard_Analysis/NSComplex.thy
changeset 76371 1ac2416e8432
parent 73926 5f71c16f0b37