[isabelle-dev] Syntax for lattice operations?
makarius at sketis.net
Sat Jun 11 21:40:43 CEST 2016
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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev