やた、やっとデバッガ的なナニカを見つけた。 https://arxiv.org/pdf/1406.0292v1.pdf

tipsつうか、jEditの常識だろうが、 変数 - 青 定数 - 黒 束縛変数 - 緑 型変数 - 紫 型定数 - 黒 キーワード - 薄めの青、緑 コメント - 茶色 内側構文 - 背景：薄い灰色 まだ評価してない - 背景：ピンク 計算中 - 背景：濃いめの紫 エラー - 背景：赤

というわけで、プログラミング言語としてのIsabelleを調べよう。1980, 90年代の資料とMLソースコードか。現在のシステムは大規模複雑だから、MLソースコードを読むのは辛い。Isabelle86のコードとか残っているといいのだが。[追記]あった。 https://www.repo…

今のIsabelleに感じる違和感と難解さって、高級指向（高級志向じゃなくて、高水準言語指向）が過ぎるせいでは？ そんな気がした。志、方向性（志向）としての高水準化、ドキュメント指向、宣言指向は否定しないが、まだ出来てないのに、ユーザーに押し付け過…

進化なのか、退行なのか？ - 檜山正幸のキマイラ飼育記 メモ編に出した Title: A Gentle Introduction to Isabelle Author: Sara Kalvala URL: http://www.informatik.uni-bremen.de/~cxl/lehre/isakurs/tutorial.ps Pages: 12 サラ・ケベレ(?)女史の1994年…

どうかしてるぜ！Isabelleマニュアルの分かりにくさも尋常ではないが、それを執拗に詮索している僕も常軌を逸しているかもな。どうかしてるぜ。Isabelleコミュニティの人は、「どうかしているぜ」な用語の曖昧さ／乱用を自覚してるのだろうか？ あまり意識し…

Pure等号の推移律はPureの公理（か定理）に入っている。"x == y ==> f x == f z" は示せなかったので、axiomatizationで公理とする。つまり、ファクト（定理データベース）の状況は、 transitiv: ?x == ?y ==> ?y == ?z ==> ?x == ?y eq_preserve: ?x == ?y …

theoremなどを使って証明した最後に結果（定理のステートメントに対応する命題シェマ）が表示されるが、axiomatizationで公理を導入すると命題シェマが表示されない。find_theorems nama: コマンドを使う必要がある。find_* コマンドを使って状況確認するっ…