[isabelle] LaTeX conversion


I have a couple questions about the latex conversion process.

1. Is there a comment syntax other than (* this *) which doesn't show up in the LaTeX file? I'd like to be able to comment-out big regions of already commented code, but since (* these *) won't nest, I don't know how to do that.

2. When I write things like "[| foo |] ==> bar", the latex converter doesn't seem to change the "[|" into the nice-looking, single symbol form, and similarly the arrow is left as ==> instead of changing it into \Longrightarrow, etc. Is there a way to get it to automatically convert these?


Jared Davis <jared at cs.utexas.edu>
3600 Greystone Drive #604 - Austin, TX 78731
(512) 879-3858

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