如何在 Isabelle 教授助手中形式化逻辑及其公理？

我有一个逻辑部分类似于线性时间逻辑，但有一些额外的东西。我想在 Isabelle 中将这个逻辑及其公理形式化。目标是在 Hilbert 演算中使用这个公理，我希望在 Isabelle 中自动化。

例如，我将有公理“G(phi1 => phi2) => (G phi1 => G phi2)”。

我想知道的是如何将这个公理形式化，以及如何使用它们来推导出公式。

很抱歉没有具体说明，但我是 Isabelle 的初学者。提前致谢。