A definite integral of the hyperbolic secant function