src/HOL/Complex/NSComplex.thy
changeset 14902 bef0dc694c48
parent 14738 83f1a514dcb4
child 15003 6145dd7538d7