src/HOL/Complex/NSComplex.thy
changeset 15552 8ab8e425410b
parent 15413 901d1bfedf09
child 17298 ad73fb6144cf