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.


	Makarius


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