*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Document preparation question*From*: Joachim Breitner <breitner at kit.edu>*Date*: Thu, 17 Jan 2013 10:19:30 +0100

Dear Isabelle users, I am adding finishing touches to an upcoming AFP entry and I am playing around a bit with Isabelle’s document generation features. It works nicely, but I have some questions: I’d like to use @{term_type foo} on expressions whose type contains a type synonym, but the result contains the unfolded type. Is there a better work-around than using @{term "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒ Env"} at {text "::"} at {typ "heap ⇒ (exp ⇒ Value) ⇒ Env"} instead of just @{term_type "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒ Env"} Also, I have trouble with no_document. My ROOT.ML reads $ cat isa-launchbury/ROOT.ML no_document use_thys ["~~/src/HOL/Library/FuncSet", "~~/src/HOL/Library/LaTeXsugar"]; use_thys ["Everything"]; And indeed, the generated files FuncSet.tex and LaTeXsugar.tex are empty. But they are included in the session_graph.pdf file. Is there a way to avoid that? The next items are more feature suggestions than question, but still: @{abbrev ..} is nice. Can we have an @{type_abbrev ..} that pretty-prints the type equations? Sometimes the lemmas would be clearer if free variables were explicitly all-quantified. Is there an easy way to achieve this (besides defining a variant of the lemma with an HOL-∀ in front)? Breaking a lemma apart with (prem 1), (prem 2) and (concl) to insert it into the text appropriately is also nice, but feels a bit dangerous – what if I later change the theory and add a premise. How about a command that asserts that a certain lemma has exactly n premises that would fail if that is no longer true? Then the careful author could use the command near places where he uses (prem 1), (prem 2) and (concl) and be sure that he presents the lemma fully. I also miss good ways to automatically print data type definitions. My work around is to show lemma Terms: "∃ x assn e'. (e = (Lam [x]. e') ∨ (e = Var x) ∨ (e = App e' x) ∨ (e = Let assn e'))" by (metis Terms.exp_assn.exhaust(1)) and pretty-print this lemma in the text, but a tool that formats an exhaust-lemma in the style of a grammar specification would be slick. Thanks, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.info.uni-karlsruhe.de/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Document preparation question***From:*Tobias Nipkow

**Re: [isabelle] Document preparation question***From:*Florian Haftmann

**Re: [isabelle] Document preparation question***From:*Christian Urban

**Re: [isabelle] Document preparation question***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Next by Date: Re: [isabelle] Document preparation question
- Previous by Thread: Re: [isabelle] Zorn's Lemma
- Next by Thread: Re: [isabelle] Document preparation question
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list