src/HOL/Complex.thy
changeset 78255 3e11f510b3f6
parent 77278 e20f5b9ad776
child 78685 07c35dec9dac