Isabelleと付き合うのは疲れる

古色蒼然たる仕様、先進的、実験的、前衛的な試みの混合物、ごった煮風。

十何年か前に「こりゃダメだ、生理的に受け付けない」と思った酷い構文も健在。

ドキュメントがPDFで読みやすいが、PDFだけ。コマンドやキーワードによる検索が出来ないで不便。PDFの検索機能と索引からのバックリンクが頼り、情けない。

あまりに入り口がたくさん有り過ぎて、どこから入っていいか分からない。僕はIsabelle/Pureから入りたいが、特定の入り口に対する解説は以外に手薄。全貌に対する俯瞰的／鳥瞰的なオーバービューも見当たらない。

[追記]文化的な背景を理解するのが大変だーー。今でもM式、S式を使っているのね。現代（21世紀）の人間にはもはや馴染みがない。きつい。[/追記]

[さらに追記]M式と思っていたのはS式でもあった。→Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか - 檜山正幸のキマイラ飼育記[/さらに追記]