src/HOL/Complex/NSComplex.thy
changeset 14360 e654599b114e
parent 14354 988aa4648597
child 14370 b0064703967b