src/HOL/Complex/CSeries.thy
changeset 23024 70435ffe077d
parent 20899 3aa6c5bfdcbb