Re: [isabelle] quotient_type command fails



On Thu, 12 Jun 2014, Lawrence Paulson wrote:

Isabelle dates from an era when no names contained white space, so it wasn’t even thought about.

I am myself too young for that, but my Compiler Construction professor used to tell us that really old versions of FORTRAN allowed white space in identifiers, which was before there was a clear concept of a "token" in programming languages. It was one of his "never do this at home" examples -- he had other ones drawn from Knuth's TeX language.


	Makarius


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