Re: [isabelle] Antiquotations and Syntax Annotations



Good to know about that! Thank you again!

On Fri, Oct 12, 2012 at 9:41 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:

> It depends on your \isabellestyle, and {it} already sets the double
> quotation
> marks to empty.
>
> Tobias
>
> Am 12/10/2012 14:35, schrieb Alfio Martini:
> > Thank you Tobias! That was a great hint! By the way, the output did not
> include
> > the quotation marks. There
> > was no need of a LaTeX workaround.
> >
> > Best!
> >
> > On Fri, Oct 12, 2012 at 9:14 AM, Tobias Nipkow <nipkow at in.tum.de
> > <mailto:nipkow at in.tum.de>> wrote:
> >
> >     You can write @{term [source] "..."} and it checks and prints your
> term as you
> >     gave it - unfortunately including the quotation marks. You can work
> around that
> >     by setting the quotation marks temporarily to empty:
> >
> >
> \newcommand{\noquotes}[1]{{\renewcommand{\isachardoublequote}{}\renewcommand{\isachardoublequoteopen}{}\renewcommand{\isachardoublequoteclose}{}#1}}
> >
> >     If you never want to see them, then you can of course do the above
> >     \renewcommands globally.
> >
> >     Tobias
> >
> >     Am 12/10/2012 13:50, schrieb Alfio Martini:
> >     > Dear Isabelle Users,
> >     >
> >     > When defining datatypes with syntax annotations, the usual
> commands @{term
> >     > "..."}, @{const "..."} present the
> >     > corresponding expressions with the alternative syntax, even if
> specified
> >     > otherwise.
> >     >
> >     > For instance, assuming the declaration below
> >     >
> >     > datatype 'a List =   Nil ("[]")
> >     >                    | Cons 'a "'a List" (infixr "#" 65)
> >     >
> >     > we have the following:
> >     >
> >     > @{term "Nil"}  produces "[]" (wanted "Nil")
> >     >
> >     > @{term "Cons"} produces "op #" (wanted "Cons") [tried @{const
> "Cons"}, but
> >     > it does not work either]
> >     >
> >     > @{term "Cons h t"} produces "(h::'a) # (t::'a List)" (wanted "Cons
> h t").
> >     >
> >     > When I want types I use term_type or show_types.
> >     >
> >     > Anyway, judging from the way the tutorial (section 4.1.1,
> definition and
> >     > discussion of "xor") I assume this kind of
> >     > control is possible with the available resources.
> >     >
> >     > I could use @{text "..."}, but this would be plain and simple
> humiliation.
> >     >
> >     > Thanks for any help on that!
> >     >
> >
> >
> >
> >
> > --
> > Alfio Ricardo Martini
> > PhD in Computer Science (TU Berlin)
> > Associate Professor at Faculty of Informatics (PUCRS)
> > Coordenador do Curso de Ciência da Computação
> > Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
> > 90619-900 -Porto Alegre - RS - Brasil
> >
>



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




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