src/HOL/Complex.thy
changeset 59774 d1b83f7ff6fe
parent 59746 ddae5727c5a9
child 59862 44b3f4fa33ca