[isabelle] How to formalize a large digraph in Isabelle?

Hi All,

The paper
https://www21.in.tum.de/~noschinl/documents/noschinski2013graphs.pdf gives
a reasonable method for formalizing small digraphs is Isabelle. By "small"
I mean a digraph which has sets of vertices and directed edges. By "large"
I mean any other kind of digraph, e.g. the graph of all sets as vertices
and all functions as directed edges. How can this be formalized in
Isabelle? Or do limitations of HOL preclude such a formalization?

Scott Constable

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.