src/HOL/Complex/Complex.thy
changeset 22143 cf58486ca11b
parent 21404 eb85850d3eb7
child 22655 83878e551c8c