src/HOL/Complex/Complex.thy
changeset 26840 ec46381f149d
parent 26311 81a0fc28b0de
child 28944 e27abf0db984