[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
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