[isabelle-dev] Syntax for lattice operations?

[Makarius]

On 11/06/16 21:26, Florian Haftmann wrote:
> After a closer look I came to conclusion that the use of Sup syntax in
> HOLCF/Porder.thy is very application-specific.  And it is a deliberate
> separate type class hierarchy since these type classes are tailored
> towards continuous function space.
> 
> So maybe the best option here is to stay with plain ASCII syntax: ‹LUB
> x∈A. f x›. – to emphasize its somewhat specific application.

Sounds fine to me.

Doing the adhoc change, I found relatively few uses of this special
HOLCF notation.


	Makarius



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160611/93de7e6f/attachment.sig>