src/HOL/Complex/NSComplex.thy
changeset 16877 e92cba1d4842
parent 15413 901d1bfedf09
child 17298 ad73fb6144cf