src/HOL/Complex.thy
changeset 56384 5fdcfffcc72e
parent 56381 0556204bc230
child 56409 36489d77c484