Checks a small Isabelle theory body and returns only relevant Isabelle output.

This wraps IsabelleClient.check_text/5 with Unicode output enabled and a small amount of routine progress-message filtering. The :from, :to, and :show_thf_app options activate the bundled TPTP/THF notation around the supplied body and restore it afterwards. Use :timeout to override the default 60 second timeout.

Converts a small THF/TPTP theory into Isabelle/HOL theory commands.

Supported annotated formulae are thf(name,type,...), thf(name,axiom,...), and thf(name,theorem/conjecture,...). Simple include('path/file.ext'). directives become imports "path/file". Formulas are preserved as THF text and quoted for Isabelle; check the result in a theory that imports "TPTP" and has unbundle from_TPTP active. Metadata after the formula may be any comma-separated TPTP terms. Bracketed metadata lists are copied verbatim into the generated Isabelle attribute brackets; non-list metadata, such as file(...) or inference(...), is ignored because it is not already in Isabelle attribute shape.

Loads the bundled TPTP.thy support theory into the active client session.

The support theory is copied into the active session's temporary directory and checked there, so later calls such as IsabelleClient.check_text/5 can import plain "TPTP" without starting a special Isabelle session.