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