# Theory Predicate_Formulas

theory Predicate_Formulas
imports
"HOL-Library.Countable"
"HOL-Library.Infinite_Set"
"HOL-Eisbach.Eisbach"
Abstract_Formula
begin
text ‹This theory contains an example instantiation of @{term Abstract_Formulas} with an
formula type with local constants. It is a rather ad-hoc type that may not be very useful to
work with, though.›
type_synonym var = nat
type_synonym lconst = nat
text ‹
We support higher order variables, in order to express ‹∀x.?P x›. But we stay first order,
i.e. the parameters of such a variables will only be instantiated with ground terms.
›