src/HOL/Real/Complex_Numbers.thy
changeset 14368 2763da611ad9
parent 14352 a8b1a44d8264