src/HOL/Complex/Complex.thy
changeset 23024 70435ffe077d
parent 22972 3e96b98d37c6
child 23123 e2e370bccde1