src/HOL/Complex.thy
changeset 75168 ff60b4acd6dd
parent 74226 38c01d7e9f5b
child 75494 eded3fe9e600