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.
>
> 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 n
Hi Makarius,
Am 11.06.2016 um 00:13 schrieb Makarius:
> On 10/03/16 11:19, Makarius wrote:
>> On Thu, 10 Mar 2016, Johannes Hölzl wrote:
>>
>>> Alternatively: Would a lattice_syntax locale work nowadays? I remember
>>> I tried it once and for some reason it didn't work. Either notations
>>> aren't
