Re: [isabelle] Document generation problems with Isabelle 2009-1

Hi Daniel,

> val show_question_marks = Unsynchronized.ref true;
> I tried copying this into ROOT.ML and changing true to false, but no
> effect. Keeping false, again no effect. So, how can I change this in my
> ROOT.ML? Is there still any possibility?

The line you must insert into your ROOT.ML is

Unsynchronized.reset show_question_marks;

If you would copy the line from term.ML, you would just allocate a new
reference of which the system won't take any notice.

> Secondly, until now I used @{thm[mode=Rule] ...} to print nice
> derivation rules for my theorems. Also, this does not work any more.

This is indeed strange, but when I rebuild the sugar document the
inference rule is printed as expected, so I do not suspect this to be
broken ;-).  If the problem persists, perhaps I could have a look at
your sources to figure out the problem.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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