src/HOL/Nonstandard_Analysis/NSComplex.thy
changeset 82083 d72a4ecf8c20
parent 73926 5f71c16f0b37