src/HOL/Complex/Complex_Main.thy
changeset 25345 dd5b851f8ef0
parent 22983 3314057c3b57
child 26118 6f94eb10adad