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

Regards
 Daniel


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

http://pp.info.uni-karlsruhe.de/

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.