2016-06-14 notation宣言 Isabelle シグネチャ（って言うかどうか知らんが）の宣言のとき、foo: "'a => 'a => X" (infix "$$" 70) のようにしてmixfix構文と優先度を指定できる。シグネチャで指定し忘れても、後からmixfixの宣言だけ出来る。 notation 名前 ( mixfix指定 )と書けばいい。mixfixの詳細は、 isar-refの"8.2.1 The general mixfix form"
