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