[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

[Lawrence Paulson]

This indeed is probably one of the chief reasons for the existing arrangements.
Larry

On 9 Feb 2011, at 08:36, Alexander Krauss wrote:

> An incompatibility that will not be reported by tests is that
> intermediate goal states, where nonzero indexnames are quite frequent,
> will look significantly different and contain many dots.