src/HOL/Complex.thy
changeset 73424 2b657a70116c
parent 73302 915b3d41dec1
child 73924 df893af36eb4