[isabelle-dev] ML tactic for eta-contracting a goal

[Makarius]

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 
required.


 	Makarius