Re: [isabelle] How do I do stone age interaction?



On Mon, 6 Dec 2010, mark at proof-technologies.com wrote:

In which document can I find a comprehensive description of the (presumably ASCII) lex (any version of Isabelle will do for starters)? And does the lex vary between logics?

If "lex" means the lexical syntax here, see the two sections called "Lexical matters" in the isar-ref manual. There are two, since Isabelle has outer and inner syntax layers.

Isabelle does not use ASCII code, but "Isabelle symbol" notation which provides an infinite alphabet of basic text entities. See the section "Strings of symbols" in the implementation manual.

This refers both to the current official release Isabelle2009-2. If you want to hear a longer story over 10-20 years of history, I can also do that.


	Makarius





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