Re: [isabelle] Display Draft in Jedit

On Sun, 20 May 2012, Christine Sherif Rizkallah wrote:

I tried display_drafts "file-name".
I get the error "Bad file name: file-name". I'm using a Mac, maybe that is
the problem.

The Mac is often a problem, but probably not this time. The following should work

  display_drafts "~~/src/HOL/ex/Seq.thy"

assuming that you have LaTeX installed.


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