### Abstract

We instantiate our syntax-independent logic infrastructure developed
in a
separate AFP entry to the FOL theory of Robinson arithmetic
(also known as Q). The latter was formalised using Nominal Isabelle by
adapting Larry
Paulsonâ€™s formalization of the Hereditarily Finite Set
theory.

BSD License