src/HOL/Complex/ComplexBin.thy
changeset 20356 21e7e9093940
parent 15140 322485b816ac