impI, assoc, transとかは、誰でもどこでも使いそうな名前なので、まずバッティングするだろう。find_theorems name: で検索して、修飾されたフルネームで指定するのが安全。

タクティク方式が分かりにくいのはサンザン指摘されているが、何故分かりにくいのか？ の分析がされてないのではないか。ユーザーは、 何に対して、 何をすべきか？ 何をしたのか？ がサッパリ把握できないのが問題なのだ。「何」に対する提示、ヒンティング…

1994年のGentle Introductionとか読むと、処理系の発展・進化はいいとして、説明や教育に関しては、退行した感がある。かつては強調されていた諸点が今は触れられなくなったのは、そのことがコミュニティの内部で常識化したせいだろう。が、新参者にとっては…