src/HOL/Complex.thy
changeset 81449 d92d754b5dd9
parent 80932 261cd8722677
child 82349 a854ca7ca7d9