src/HOL/Complex/CStar.thy
changeset 21404 eb85850d3eb7
parent 20732 275f9bd2ead9
child 21830 e38f0226e956