src/HOL/Complex.thy
changeset 74116 5cd8b5cd0451
parent 73928 3b76524f5a85
child 74223 527088d4a89b