Isabelleをいじっているあいだ（＝飽きるまで ^^;）は、ダイアリーにIsabelleの話が入るでしょう。今日は小ネタ。「ハイコンテキストな定数・記号の解釈」とかで話題にしたmin-plus半環をIsabelleで書いてみました。あの記事では、通常の演算子記号「+」「*…