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
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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