Re: [isabelle] Does Isabelle (on Proof general) support comments in



> The experts tell me that the Proof General - Isabelle link does not tolerate
> unicode. There is a certain chance that the next release due in the near
> future will solve this problem although the experts don't want to be quoted
> on this. Then you can input Chinese comments.
> Sorry about the later answer and the inconvenience.
FYI: I just experimented a little bit: UTF-8 seems to work well (SJIS encoding
was problematic in batch mode) if you only use 16bit characters within comments 
(either ML-style or "text{* *}"). I just created a theory with Japanese 
comments; therefore it should also work with Chinese. 
Albeit, using Japanese characters within HOL forumlae gave weird results :-). 

Achim






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