Abstract
We present a formalization of Menger's Theorem for directed and
undirected graphs in Isabelle/HOL. This well-known result shows that
if two non-adjacent distinct vertices u, v in a directed graph have no
separator smaller than n, then there exist n internally
vertex-disjoint paths from u to v. The version for undirected graphs
follows immediately because undirected graphs are a special case of
directed graphs.