title: What is the automation support for theories other than HOL in Isabelle?
body: <p>According to my scan of the Isabelle files, the Sledgehammer tool is only available for Isabelle/HOL. I'm curious about the automation of other theories in Isabelle. For instance:</p>
  <ul>
  <li>Isabelle/ZF</li>
  <li>Isabelle/FOL</li>
  </ul>
  <p>Do they support:</p>
  <ul>
  <li>automatic provers</li>
  <li>SMT solvers</li>
  <li>specialized decision procedures</li>
  </ul>