src/HOL/Complex/Complex.thy
changeset 27416 07e04ab0177a
parent 26311 81a0fc28b0de
child 28944 e27abf0db984