Re: [isabelle] Error when using \<sqinter> instead of inf

Hi Viorel,

> Thank you for the quick answer. Is there a drawback to import
> Lattice_Syntax? I see that the pretty syntax is used in the HOL
> lattice files and I expected to work if I import Lattices.

in the HOL theorie the lattice syntax is deleted ("no_notation") at the
end of each lattice section.  Once there was a fundamental decision not
to enrich the syntax universe of the HOL theories any more, in order
that users stay free to use it after their fashion.  This of course does
not solve the fundamental problem of how to control syntax
appropriately, but it is a usable compromise.

Hope this helps



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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