src/HOL/Complex.thy
changeset 55101 57c875e488bd
parent 54489 03ff4d1e6784
child 55734 3f5b2745d659