# [isabelle] Mixfix syntax with fewer arguments

Hi all,

`I am preparing a paper based on some of my Isabelle theories with the
``isatool facility to generate LaTeX. A problem that I am frequently
``facing is that I want to hide the constant name completely from the
``paper and just fancy notation. However, I often do not want to supply
``all parameters to some function and still get the notation.
`

`For example, suppose there are two definitions, one of which is with
``mixfix 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 symbols
``instead 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 is
``not given all parameters. Those parameters which are missing should be
``replaced by some placeholder (like _, but . or \cdot would equally do.
``The simple way would clearly be to write @{text "a |- b : _ *"}, but in
``thm-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 "_ |- _ : _ *", "foo
``a" to "a |- _ : _ *", "foo a b" to "a |- b : _ *" and so on?
`
Thanks in advance,
Andreas

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