Re: [isabelle] Problems with Logic.mk_implies + compose_tac

On Mon, 11 Jul 2011, Holger Gast wrote:

The function Goal.prove_internal is merely a wrapper for Goal.init / Goal.conclude (+ introducing & discharging assumptions), and init/conclude perform the internal fiddling with the invisible protect constant for you. A quick grep over the sources shows that prove_internal and compose_tac are used by tools and internal code, presumably to do similar low-level goal manipulations.

Grepping through the sources (or using hypersearch in jEdit) is indeed very important to get an idea how common certain operations are.

Goal.prove_internal shows up very rarely, in special situations or ported versions of quite old tools (the latter aspect can be seen from the Mercurial history, if this extra time is spent with it).

We are getting at an interesting collection of odds and ends of internal system tools. I maintain that it is possible to ignore all this for regular applications, and just use the standard system structures around the Pure rule calculus and its goal format, without lots of workarounds.


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