src/HOL/Complex.thy
changeset 57354 ded92100ffd7
parent 57259 3a448982a74a
child 57512 cc97b347b301