src/HOL/Complex/Complex.thy
changeset 20531 7de9caf4fd78
parent 20485 3078fd2eec7b
child 20556 2e8227b81bf1