src/HOL/Complex.thy
changeset 77300 57467fdd507d
parent 77221 0cdb384bf56a
child 77278 e20f5b9ad776