Re: [isabelle] locales and proofs programming bugs

On Fri, 4 May 2012, Bill Richter wrote:

When I code in jedit, I use fancy symbols like ∀, but in the file, jedit seems to replace ∀ by \<forall>. Is there a way to change that?

The prover refrains from using Unicode on its own, but the front-end may do so based on certain translation tables. These are given as defaults in ISABELLE_HOME/etc/symbols and ISABELLE_HOME_USER/etc/symbols, so in principle this can be changed.

As a new user you should not try that, though, unless you want to spend most of the time tinkering with the system instead of using it.


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