src/HOL/Complex/CStar.thy
changeset 22522 783c8dbe3ade
parent 21848 b35faf14a89f