Re: [isabelle] Isabelle2014-RC0 available for testing
On Tue, 8 Jul 2014, Joachim Breitner wrote:
* I just observed an error message in the output window:
Undefined constant: "list.size"⌂
And I wonder what the ⌂ is about.
General PIDE principle: use C-hover to ask about what you see. Here it
will give you a visual clue that it is a hyperlink -- the one stemming
from a symbolic position.
IIRC, there is no explicit documentation of this new \<here> (or "house" /
"home") symbol, but the general principles are now quite explicit in the
This archive was generated by a fusion of
Pipermail (Mailman edition) and