src/HOL/Complex/NSComplex.thy
changeset 17357 ee2bdca144c7
parent 17332 4910cf8c0cd2
child 17373 27509e72f29e