Examples (8)
■ tacticをtheorem_tacticとして用いる方法
tactic tacの書式はtac goalstack,
theorem_tactic ttacの書式はttac thm goalstackなので,
ttac thmがcurryingによりtacticになっている訳です.
従って,(fun (t:thm)->tac)とすればtheorem_tacticが得られます.
■ tacticをtheorem_tacticとして用いる方法
tactic tacの書式はtac goalstack,
theorem_tactic ttacの書式はttac thm goalstackなので,
ttac thmがcurryingによりtacticになっている訳です.
従って,(fun (t:thm)->tac)とすればtheorem_tacticが得られます.