Re: [isabelle-dev] Syntax for lattice operations?

2016-06-12 Thread Tobias Nipkow
On 12/06/2016 18:22, Florian Haftmann wrote: Thus I would like to understand why we cannot reuse Sup etc in HOLCF like we do for all the other variants of lattices we have. We would probably need a suitable type class because at the moment lub is unrestricted. For each type class, per type

Re: [isabelle-dev] Syntax for lattice operations?

2016-06-12 Thread Florian Haftmann
> Thus I would like to understand why we cannot reuse Sup etc in HOLCF > like we do for all the other variants of lattices we have. We would > probably need a suitable type class because at the moment lub is > unrestricted. For each type class, per type constructor there is at most *one*

Re: [isabelle-dev] Syntax for lattice operations?

2016-06-12 Thread Tobias Nipkow
On 11/06/2016 21:26, Florian Haftmann wrote: 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

Re: [isabelle-dev] Syntax for lattice operations?

2016-06-11 Thread Florian Haftmann
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 >>>

Re: [isabelle-dev] Syntax for lattice operations?

2016-06-10 Thread 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 supported in locales or they are exported after the context

Re: [isabelle-dev] Syntax for lattice operations?

2016-03-13 Thread Tobias Nipkow
On 10/03/2016 11:00, Florian Haftmann wrote: Hi all, traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been kept in a separate library theory, to allow use of that quite generic notation for unforeseen applications. Meanwhile however all those operations to which

Re: [isabelle-dev] Syntax for lattice operations?

2016-03-10 Thread Makarius
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 supported in locales or they are exported after the context -block. The concept of 'bundle' was

Re: [isabelle-dev] Syntax for lattice operations?

2016-03-10 Thread Florian Haftmann
> What would be the objective of this change? Mainly to get rid of those brittle (no_)notation declarations scattered over various theories. Organizing syntax through library theories does not quite work out. Florian > >> On 10 Mar 2016, at 10:00, Florian Haftmann >>

Re: [isabelle-dev] Syntax for lattice operations?

2016-03-10 Thread Lawrence Paulson
What would be the objective of this change? Larry > On 10 Mar 2016, at 10:00, Florian Haftmann > wrote: > > Hi all, > > traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been > kept in a separate library theory, to allow

Re: [isabelle-dev] Syntax for lattice operations?

2016-03-10 Thread Johannes Hölzl
Am Donnerstag, den 10.03.2016, 11:00 +0100 schrieb Florian Haftmann: > Hi all, > > > traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been > kept in a separate library theory, to allow use of that quite generic > notation for unforeseen applications. > > Meanwhile

[isabelle-dev] Syntax for lattice operations?

2016-03-10 Thread Florian Haftmann
Hi all, traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been kept in a separate library theory, to allow use of that quite generic notation for unforeseen applications. Meanwhile however all those operations to which that syntax is attached to are members of