Re: [isabelle] lexical matters



On 18/01/11 09:34, mark at proof-technologies.com wrote:
It puzzles me how little has been done about these things until now.  Are
not people concerned that what is being displayed could be misleading?

No.

If one has reason to suspect that something funny might be going on, the terms in question can be examined using the primitive ML API.

Alternatively, one can print the term out using a primitive pretty-printer that doesn't attempt to do anything "fancy".

For example, in HOL4 one can use

  Parse.print_term_by_grammar min_grammars

Michael





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