[isabelle] Document generation problems with Isabelle 2009-1

Hello everyone,

after moving to Isabelle 2009-1, I experience many problems with document generation. First, I'd like the question marks in printed theorems to disappear. Until now, I just wrote "reset show_question_marks" in my ROOT.ML, and all was good. Now, ML won't accept reset any more. I found something in the NEWS, saying that show_question_marks is now a flag, and in Pure's term.ML, I found the following line:
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?

Secondly, until now I used @{thm[mode=Rule] ...} to print nice derivation rules for my theorems. Also, this does not work any more. The documentation on the Isabelle website still shows this as the way to go, and I found nothing in the NEWS describing this problem...

I'm glad to accept any advice :)
..and perhaps the one changing the whole document preperation stuff writes also an updated LaTeXSugar document...


Karlsruher Institut für Technologie (KIT) IPD Snelting

Daniel Wasserrab

wissenschaftlicher Mitarbeiter

Adenauerring 20a, Gebäude 50.41, Raum 022
76131 Karlsruhe

Telefon: +49 721 608-7399
Fax: +49 721 608-8457
E-Mail: daniel.wasserrab at kit.edu


KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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