src/HOL/Complex.thy
changeset 75828 298707451ec2
parent 75543 1910054f8c39
child 76376 934d4aed8497