昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。 内容: Isabelleの独自な世界 Isabelleの未来 Isabelleの独自な世界 「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より: PIDE構想は、Isabelleプロジェクト/コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか? なかなかに興味深いですな。 Isabelleが世の趨勢と離れるのか?
![Isabelleについて: 証明支援系は何を目指し、どこへ向かうのか - 檜山正幸のキマイラ飼育記 (はてなBlog)](https://cdn-ak-scissors.b.st-hatena.com/image/square/28e6ef01cef4d74f219935cfe183c76adc9bd1bd/height=288;version=1;width=512/http%3A%2F%2Fwww.chimaira.org%2Fimg3%2Fisabelle-output-1.png)