Re: [isabelle] LaTeX conversion

On Fri, 29 Sep 2006, Jared Davis wrote:

> 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.

(* *) do nest as in ML.  The only problem is that Emacs / ProofGeneral 
might be confused by this.  Some versions should work, despite the 
misleading font-lock display.

An alternative is to markup LaTeX output to be invisibile, e.g. like this:

  text %invisible {* ... *}

Note that {* ... *} does not nest, and the content needs to be legal 
source in terms of the document preparation system.

> 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?

No.  The document system merely presents the sources as they are written. 
An alternative is to let the system output formal entities using 
antiquatations, e.g. @{thm foo} -- here the output is subject to the 
xsymbols/latex print mode.


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