refinement

やっと分かった、refinement という言葉。定義はなかった。「悟れ」ということらしい。要するに、未完成の証明図を考えて、未完成部分に「・・・」のようなマーカーがあるとして、そのマーカー部分＝未完成の部分を埋める作業をrefinementと言っているらしい。

[追記]goalのresolutionもrefinementなのかもしれない。tacticのやることは何でもrefinementとか？[/追記]