Re: [isabelle] Isabelle document preparation

On Thu, 22 Jan 2009, Peter Lammich wrote:

> I have a problem with the latex-document generated by Isabelle.
>    No space is put in between inner-syntax blocks, i.e. if I have the
> following:
> lemma
>  assumes "P x" "f x"
> it will look in latex like:
>  lemma
>    assumes P x f x
> That can be very confusing! Is there some tuning option to put some 
> extra space, or perhaps a ";\ \ " in between such lists. The only 
> workaround I know up to now is to put each such inner-syntax block in 
> its own line, what makes the proofs more unreadable at editing time.

The problem here is that the document preparation system does not really 
understand the structure of the text -- it is basically just a mock-up, 
but few people have noticed in the past decade :-)

There are some possibilities nonetheless:

  (1) Write your sources with extra space between adjacent propositions, 
  i.e. assumes "P x"  "f x"; this is what I usually do, unless the 
  exdplicit 'and' solution is possible.

  (2) Use a LaTeX style that does not hide the quotes.  This is just a 
  matter of definining \isachardoublequoteopen and 
  \isachardoublequoteclose in a suitable way; see the examples in 

  Of course you can render the quotes in any way you see fit, e.g. funny 

  (3) Run perl over the generated LaTeX sources to replace adjacent 
  {\isachardoublequoteclose} and {\isachardoublequoteopen} -- a bit 
  fragile, but often works for individual papers, theses etc. that are 
  prepared with special care.


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