src/HOL/Complex.thy
changeset 76768 40c8275f0131
parent 76722 b1d57dd345e1
child 77138 c8597292cd41