Re: [isabelle] quotient_type command fails

Up to now Isabelle never complained about whitespace in theory names, so I assumed that this is supported.

IMHO Isabelle should either immediately complain about the whitespace or quotient_type should work as expected. Anything else feels a bit inconsistent.

Apart from that:

Guessing from the error output, I would say that some function is splitting the string containing theory names using whitespace as delimiter. Thus ends up with the theory name "Whitespace" and loses the "With " part.

Salomon Sickert

On 2014-06-11 12:51, Lawrence Paulson wrote:
I don’t think that any names in Isabelle are allowed to contain whitespace.

Larry Paulson

On 10 Jun 2014, at 10:20, Salomon Sickert <sickert at> wrote:

Apparently in Isabelle 2013-2 the quotient_type command doesn't work, if the theory name contains white-space.

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