unicode_fol_kit.to_isabelle_modal

unicode_fol_kit.to_isabelle_modal(formula, mode='constant', frame='K')[source]

Emit a complete, loadable Isabelle/HOL theory shallow-embedding formula.

This delegates to unicode_fol_kit.hol.isabelle_modal.to_isabelle_modal() — the real, full-modal-family exporter that emits a loadable theory … begin … end with every lifted operator defined and a genuine lemma (it replaced the earlier alethic-only skeleton). Use that module directly for the additional options (epistemic/doxastic/deontic/temporal coverage, the proof tactic, temporal_closure).

Parameters:
Return type:

str