src/HOL/Complex/Complex.thy
changeset 21316 4d913b8bccf1
parent 20763 052b348a98a9
child 21404 eb85850d3eb7