Isar ではassume、ゴールの前提を使用して、結論を構築することができます。
assume expects to be able to unify with existing premises in the goal
これが の唯一の使用法ですかassume、つまり、ゴールの前提から事実を取得することですか?
更新：これは広すぎると考える人もいるので、私には理解できません。質問を再定式化しようとします。
このマニュアルでは、 の論理的な内容について説明していますassume。しかし、その使用法は何ですか？それは、ゴールの前提から事実を得た場合に限られますか？