src/HOL/Complex.thy
changeset 69619 3f7d8e05e0f2
parent 69260 0a9688695a1b
child 70707 125705f5965f