Re: [isabelle] Generating .tex from .thy without a proper session


Am Montag, den 11.02.2013, 17:33 +0100 schrieb Makarius:
> For example, you can print formal entities with the "latex" print mode 
> interactively like this:
>    thm (latex) exI exE
> or goal states:
>    pr (latex)
> This is a half-forgotten and quite archaic form.  I can't tell on the 
> spot how far it still works.

It works, just today I was using "thm (latex)" quite a few times where I
really just need a theorem, and not a whole Isar command.

> > Is there a low-level-command that goes from .thy directly to .tex, 
> > without a session infrastructure involving ROOT and document/root.tex?
> That is difficult with the full spectrum of document antiquotations etc. 
> The main entry point for that is Thy_Output.present_thy but that is not 
> easily invoked manually.
> Proper document preparation is still intertwined with the session concept, 
> although there is conceptually no strong reason for it, just old habits.
> In the past few years, I have occasionally made tiny steps to make it more 
> value oriented, operating on given sources more systematically.  My 
> immediate motivation is to have document preparation within the Prover 
> IDE, to avoid the relatively clumsy batch build sessions.

Thanks, that would be great. Until then, "isabelle mkroot -d" followed
by adding Scratch to the theories and quick_and_dirty to the options is


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

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

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