*To*: Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>*Subject*: Re: [isabelle] Mixfix syntax with fewer arguments*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 14 May 2008 10:32:17 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <482972B2.2070306@ipd.info.uni-karlsruhe.de>*References*: <482972B2.2070306@ipd.info.uni-karlsruhe.de>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

I don't think there is any way to achieve automatically what you want.

Tobias Andreas Lochbihler wrote:

Hi all,I am preparing a paper based on some of my Isabelle theories with theisatool facility to generate LaTeX. A problem that I am frequentlyfacing is that I want to hide the constant name completely from thepaper and just fancy notation. However, I often do not want to supplyall parameters to some function and still get the notation.For example, suppose there are two definitions, one of which is withmixfix syntax, and some text...definition foo :: "'a => 'b => 'c => bool" ("_ |- _ : _ *" [50, 0, 20] 70) where "a |- b : c * == True" definition bar :: "'a => ('a => 'b => 'c => bool) => bool" where "bar a f == !b c. f a b c" text {* @{term "foo a b"} is a predicate on @{typ 'c} saying that ... @{term "bar a foo"} denotes that @{term "foo a"} holds everywhere. *}What I would like the text to be typeset (with appropriate LaTeX symbolsinstead of the ASCII art) is:"a |- b : _ * is a predicate on 'c saying that ... bar a (_ |- _ : _ *) denotes that a |- _ : _ * holds everywhere."I.e. I would like to have the mixfix syntax printed even though foo isnot given all parameters. Those parameters which are missing should bereplaced by some placeholder (like _, but . or \cdot would equally do.The simple way would clearly be to write @{text "a |- b : _ *"}, but inthm-antiquotations, this trick does not work, e.g.lemma foo: "foo a b = (%x. True)" by(auto intro: ext simp add: foo_def) text {* @{thm foo} *} should produce "?a |- ?b : _ * = (%x. True)".How can I have "foo" (automatically) translated to "_ |- _ : _ *", "fooa" to "a |- _ : _ *", "foo a b" to "a |- b : _ *" and so on?Thanks in advance, Andreas

**References**:**[isabelle] Mixfix syntax with fewer arguments***From:*Andreas Lochbihler

- Previous by Date: [isabelle] about th proof of protocol
- Next by Date: Re: [isabelle] Lemmas in locales
- Previous by Thread: [isabelle] Mixfix syntax with fewer arguments
- Next by Thread: [isabelle] Lemmas in locales
- Cl-isabelle-users May 2008 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