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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
