誘導規則のケース名（Isabelle）

Question

一部の誘導規則には大文字と小文字の区別があります。デフォルトの規則の例は、case 0とcase (Suc n)です。与えられた規則、例えば。 int_induct、この補助定理を含む理論を見ずに、どのようにして（実際にはそれがあるのか​​）そのケースの名前を知ることができますか？

Answer 1

これを行うための高度な方法はわかりません。

ML‹Thm.get_tags @{thm nat.induct}› 

この版画：あなたが見ることができるように

val it = [("name", "Nat.nat.induct"), ("kind", "theorem"), ("case_names", "zero;Suc")]: Properties.T 

は、ケースの名前がキーで市販されているケース名はタグMLで得ることができる定理のに格納されていますcase_names。