[isabelle] How to formalize a large digraph in Isabelle?
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and