Isabelle ゆるリファレンス（apply-scriptスタイル） - 若くない何かの悩み

最近は本業の自動テストマンより定理証明支援系に力を入れている Kuniwak です（経緯は過去記事参照）。 orgachem.hatenablog.com 定理証明支援系はいいぞ、ということで本記事では 私がよく使う Isabelle の便利機能の紹介とごく個人的に感じている使い所などを書いています。 そのため全機能を網羅するものではなくかなり漏れがあります。もし「これめっちゃ便利だけど書いてない！」みたいな気づきがありましたらご指摘いただけると嬉しいです！ 本記事の対象読者 対象読者は Isabelle の apply-script スタイルを学びたい方で、かつ「Tutorial on Isabelle/HOL 2020 の 1, 2, 3, 5 章を読んでなんとなくわかったけど…」な方です。もし定理証明支援系を使ったことがなく、Tutorial もまだ読んでいない方は 1, 2, 3,

[devorgachem]

定理証明支援系はいいぞ、ということで書きました