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
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.
On 2014-06-11 12:51, Lawrence Paulson wrote:
I don’t think that any names in Isabelle are allowed to contain
On 10 Jun 2014, at 10:20, Salomon Sickert <sickert at in.tum.de> 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