[isabelle] entering symbols in Isabelle/jEdit



Hi,

 

I have thought of a small feature for entering symbols. If you have a system
of theories with your own notation, you use a handful of symbols. 

 

In the symbols windows, there could be a tab that shows your infix symbols,
but that would require to process the read theories, and a question would
arise: to what extent, down to the HOL library?

 

An easier solution would be to have a "recently used" tab in the symbols
window that would show the ones you started to use. It could ease entering
your own notation.

 

What do you think of this? Is there a builtin solution for this problem?

 

- Gergely




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