src/HOL/Complex/Complex.thy
changeset 15187 8b74a39dba89
parent 15140 322485b816ac
child 15234 ec91a90c604e