Re: [isabelle] resolve current subgoal with matching premise



On Fri, 5 Dec 2014, Dmitriy Traytel wrote:

Well, the Subgoal.FOCUS combinator gives one at least some structure (fixes and assumes) in the hands.

That is indeed one of the main entry points for structured proofs in Isabelle/ML. The "implementation" manual has some further text on it in section "6.3 Structured goals and results".

The goal focus is often in conflict with schematic goals, but these are very esceptional anyway.


	Makarius

----------------------------------------------------------------------------
                http://stop-ttip.org  1,151,699 people so far
----------------------------------------------------------------------------




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.