src/HOL/Complex.thy
changeset 70759 26837fd025a3
parent 70707 125705f5965f
child 70802 160eaf566bcb