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
This archive was generated by a fusion of
Pipermail (Mailman edition) and