[isabelle-dev] ML tactic for eta-contracting a goal
makarius at sketis.net
Tue May 25 13:39:25 CEST 2010
On Sat, 22 May 2010, Brian Huffman wrote:
> I think I just found answer to my question:
> fun eta_tac i = CONVERSION Thm.eta_conversion i
> I had never used "CONVERSION" until now. I guess that what it does is
> apply the conversion to the entire subgoal?
Yes, using the CONVERSION combinator is the canonical way to let a
conversion operate on a subgoal, and present the whole thing as a tactic.
Grepping for it through the sources you will find some typical
applications. In order to prevent duplication of common conversions as
tactics in the ML environment, it is also customary to inline that
composition, e.g. use (CONVERSION Thm.eta_conversion) directly where
More information about the isabelle-dev