ネットで参照できる Isabelle の解説は非常に充実していますが，日本語となると数える程しかありません．スライドでないものだと，ちょっと古いですが．．． http://www.ieice-hbkb.org/files/07/07gun_01hen_02.pdf http://www.score.is.tsukuba.ac.jp/~min…

これも HOL Light で書いた定理ですが，Isar では．．． theory convex imports Complex_Main begin theorem convex: fixes a b :: real and n :: nat assumes "0 <= a" and "0 <= b" shows "((a + b) / 2) ^ n <= (a ^ n + b ^ n) / 2" (is "?L n <= ?R n")…