Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Elbe with Symbols


view this post on Zulip Email Gateway (Aug 18 2022 at 18:55):

From: Jens Doll <jd@cococo.de>
Hello,

the next version of the Elbe software will contain a more comfortable
editor for Isabelle source files. It is planned to have a fully
functional editor for special characters. The sources will stay ASCII
files and in the editor the special chars will be represented by their
glyphs. On save these glyphs will become substituted by ASCII symbols.
You can have a look at the current layout under

https://www.cococo.de/products/windows/Columbo/sample6.html

Two questions arose:

a) are the chars shown all chars used in Isabelle?
b) What does <^const> mean? I did not find it in the table ..

Happy reasoning in 2012,
Jens

view this post on Zulip Email Gateway (Aug 18 2022 at 18:55):

From: Makarius <makarius@sketis.net>
There are some explanations and specifications on this in
the isar-ref manual (appendix B) and the implementation manual (section
1.2.1), see also http://isabelle.in.tum.de/documentation.html

It is also advisable to check how the Isabelle/jEdit Prover IDE handles
this issue -- there is a brief overview in the README on startup. This is
based on a general module in Isabelle/Scala, see also
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011-1/src/Pure/General/symbol.scala

Makarius


Last updated: Mar 29 2024 at 08:18 UTC