src/HOL/ex/Landau.thy
changeset 46368 ded0390eceae
parent 41413 64cd30d6b0b8