*To*: Joachim Breitner <breitner at kit.edu>*Subject*: Re: [isabelle] Document preparation question*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 17 Jan 2013 11:03:56 +0100*Cc*: Isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <1358414370.4392.23.camel@kirk>*Organization*: TU Munich*References*: <1358414370.4392.23.camel@kirk>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130106 Thunderbird/17.0.2

Hi 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"} I would suggest @{term_type [source] "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒ Env"} > @{abbrev ..} is nice. Can we have an @{type_abbrev ..} that > pretty-prints the type equations? Something to think about. > 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)? You could write a style in ML for the term antiquotation to add the quantifiers to propositions. See the LaTeX sugar document for fundamental hints, or just get back here. > 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. Maybe also something which can be implemented as term style, e.g. expecting an exhaustivness lemma as produced by datatype and rearranging it as desired. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Document preparation question***From:*Joachim Breitner

**References**:**[isabelle] Document preparation question***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Document preparation question
- Next by Date: Re: [isabelle] Document preparation question
- Previous by Thread: Re: [isabelle] Document preparation question
- 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