src/HOL/Complex.thy
changeset 73443 8948519e0a78
parent 73302 915b3d41dec1
child 73924 df893af36eb4