src/HOL/Complex/Complex.thy
changeset 27125 0733f575b51e
parent 26311 81a0fc28b0de
child 28944 e27abf0db984