src/HOL/Complex/ComplexBin.thy
changeset 22452 8a86fd2a1bf0
parent 15140 322485b816ac