  We present the first verified implementation of a decision procedure for the
quantifier-free theory of partial and linear orders. We formalise the procedure
in Isabelle/HOL and provide a specification that is made executable using
Isabelle's code generator. The procedure is already part of the development
version of Isabelle as a sub-procedure of the simplifier.
