src/HOL/Complex/CStar.thy
changeset 23563 42f2f90b51a6
parent 21848 b35faf14a89f