[isabelle-dev] Syntax for lattice operations?

[Florian Haftmann]

> For the moment I think bold syntax in the first choice.  In the middle
> run I would suggest to have a closer look at HOLCF/Porder.thy to see
> whether something can be done to integrate it more with the standard
> type classes;  a least it formalizes a lot about upper / lower bounds
> which is not HOLCF-specific in any way, so it could go to HOL/Library
> for example.

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.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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/e9506bc5/attachment.sig>