src/HOL/Complex/NSComplex.thy
changeset 15678 28cc2314c7ff
parent 15413 901d1bfedf09
child 17298 ad73fb6144cf