src/HOL/Complex/ex/BigO_Complex.thy
changeset 28667 4adfdd666e7d
parent 26806 40b411ec05aa