Re: [isabelle] quotient_type command fails



Isabelle dates from an era when no names contained white space, so it wasn’t even thought about. The development team will have to think about whether whitespace in theory names is worth supporting or not.

Larry Paulson


On 11 Jun 2014, at 18:44, Salomon Sickert <sickert at in.tum.de> wrote:

> 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.
> 
> Regards,
> 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 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 MHonArc.