ONCE_DEPTH_CONV c applies c to only the first suitable subterm(s) found in a top-down search, i.e. the outermost subterm(s). # ONCE_DEPTH_CONV BETA_CONV `(\x. x+1) ((\y. y+2) 3)`;; val it : thm = |- (\x. x + 1) ((\y. y + 2) 3) = (\y. y + 2…

A conversion takes a term and returns an equality theorem with the term on the lhs (or it fails).NO_CONV is a conversion which always fails. # NO_CONV `0`;; Exception: Failure "NO_CONV". ALL_CONV is a conversion which always succeeds witho…

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