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