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

Lawrence Paulson lp15 at cam.ac.uk
Wed Feb 9 09:40:01 CET 2011

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

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. 

More information about the isabelle-dev mailing list