Re: [isabelle] unicode tokens in isabelle2011+pg4.0


Am Dienstag, den 01.02.2011, 22:02 +0100 schrieb Alexander Krauss:
> I am not sure if I know a solution, but the problem seems to be that you 
> are creating a unicode symbol in the buffer, but Isabelle expects the 
> ascii-encoded symbol \<forall> (which pg displays using the same glyph, 
> but it's represented differently). I can reproduce this without special 
> keyboard mapping by copy and pasting the character from elsewhere. 

is there a reason why Isabelle would not accept ∀ synonymously to
\<forall> in theory files? This would also be nice for all those
unicode-loving folk who occasionally at .thy files directly (e.g. doing
some mass-substitution with vim, or looking at diffs).


Joachim Breitner
  e-Mail: mail at
  ICQ#: 74513189
  Jabber-ID: nomeata at

Attachment: signature.asc
Description: This is a digitally signed message part

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