src/HOL/Complex.thy
changeset 73428 9d1b5c0bdec8
parent 73302 915b3d41dec1
child 73924 df893af36eb4