2010-04-17から1日間の記事一覧

Isabelle Tutorial その15

5.17 Managing Large Proof 長くなりがちな証明のステップを短くする方法を見ていきます。 5.17.1 Tacticals, or Control Structures 長い証明の中には、規則性が現れることがあります。プラス記号(+)を使用して、ステップを繰り返すことができます。例えば…