[isabelle] Document preparation question

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.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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