src/HOL/Complex/CStar.thy
changeset 26840 ec46381f149d
parent 21848 b35faf14a89f