# Has the compactness theorem for FOL been formalized in Coq/Isabelle/etc?

I've been searching for a formalization of the compactness theorem for FOL, but haven't found any. Is anyone aware of such a development or related work?

-
Have you tried asking on the Coq or Isabelle mailing lists? –  Dave Clarke Feb 3 '12 at 9:42
I am not sure if this is suitable for cstheory, but see this. Completeness is there, and compactness is not far from it. –  Kaveh Feb 5 '12 at 5:30
See also the AFP entry for a version in Isabelle/HOL (from 2004). –  Makarius Mar 4 '13 at 11:09