*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Dysfunctional complete lattice syntax [was: Isabelle2016-RC0 available for testing]*From*: Makarius <makarius at sketis.net>*Date*: Sun, 3 Jan 2016 22:15:32 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5689428E.7040102@informatik.tu-muenchen.de>*References*: <alpine.LNX.2.00.1601011959030.31080@lxbroy10.informatik.tu-muenchen.de> <5689428E.7040102@informatik.tu-muenchen.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Sun, 3 Jan 2016, Florian Haftmann wrote:

The quite recent de-ASCII-fication of symbols produced a collateral damage, illustrated with the following snippet: theory Foo imports Main begin term "INFIMUM A (Îx. f x x)" The problem is that we had the tradition to add (and remove) pretty lattice syntax by need (cf. also theory Lattice_Syntax in HOL-Library), falling back to ASCII syntax by default.

I can forsee two solutions: * retain ASCII syntax for INFIMUM, SUPREMUM; * make pretty lattice syntax standard; this seems feasible since we have syntactic type classes for all lattice operators anyway, but I guess applications still contain definitions which do not match the type of the polymorphic operators.

Makarius

**Follow-Ups**:

**References**:**[isabelle] Isabelle2016-RC0 available for testing***From:*Makarius

**[isabelle] Dysfunctional complete lattice syntax [was: Isabelle2016-RC0 available for testing]***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Isabelle2016-RC0 - A fast implementation of concat for strings?
- Next by Date: Re: [isabelle] Isabelle2016-RC0 - does not exit on Linux
- Previous by Thread: [isabelle] Dysfunctional complete lattice syntax [was: Isabelle2016-RC0 available for testing]
- Next by Thread: Re: [isabelle] Dysfunctional complete lattice syntax [was: Isabelle2016-RC0 available for testing]
- Cl-isabelle-users January 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list