[isabelle] Presenting theories without running a session



Hello, Isabelle users,

I am curious about converting .thy files to .tex files without running a
session to verify the document (with Isabelle 2011).  Is this possible?  I
have been looking at the documentation for 'isabelle make', 'isabelle
usedir', 'isabelle document', and 'isabelle latex', but I cannot conclude if
producing LaTeX code depends on processing the documents, producing the
heap, and so on.  Clearly, running the following is sufficient to produce
the .tex files.  What is necessary?

isabelle usedir -D generated HOL Foo
>


As an aside, here is something I noticed about the behavior of the isabelle
command line tool.  I can work around it, I am just sharing it for your
information as a possible bug: typing 'isabelle' at a command prompt gives
usage information, and includes the message 'pass "-?" for tool specific
help.'  But if I type, say, 'isabelle usedir -?', it gives the following
message along with the expected usage info for usedir:

/scratch/usr/Isabelle2011/lib/Tools/usedir: illegal option -- ?
>

That is in bash.  In my favored shell, zsh, the shell gives an error because
it thinks the ? is a wildcard.

Take care,
Robert




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