# Re: [isabelle] Document preparation question

Dear Joachim,
> 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"}

`type_synonym declarations only introduce the parse translations for type
``abbreviations. The print direction like for term abbreviations is not
``produced automatically, but you can add it manually:
`
translations (latex)
(type) heap <= (type) "(var * expr) list"

`However, this translation will be applied to all printed type in the
``given print mode (latex in the example), so any occurrence of (var *
``expr) list" will be printed as "heap". This is similar to printing
``abbreviations on the term level. With this translation in place,
``@{term_type "heapToEnv :: heap => (exp => Value) => Env"} should print
``what you expect.
`

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?

`I know one way to avoid that: Build a heap image with all auxiliary
``theories that you do not want to show up in session_graph.pdf, i.e., HOL
``with FuncSet and LaTeXsugar, and then base your session on this image.
`

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.

`You don't have to state and prove this lemma yourself, the datatype
``package generates a similar one called expr.nchotomy for type expr.
`
Andreas

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