[isabelle] Dysfunctional complete lattice syntax [was: Isabelle2016-RC0 available for testing]



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.

Cheers,
	Florian	

Am 01.01.2016 um 20:17 schrieb Makarius:
> Dear Isabelle users,
> 
> the coming Isabelle2016 release is scheduled for February 2016, after
> the next big Java 8 update by Oracle in January and some weeks before
> the deadline of ITP 2016.
> 
> To get started with systematic testing there is now the relatively early
> http://isabelle.in.tum.de/website-Isabelle2016-RC0 (corresponding to
> Isabelle/e18444532fce and AFP/c62777f3e932).
> 
> The website, NEWS, ANNOUNCE etc. are already mostly up-to-date.  Some
> documentation is still lagging behind, notably the Isabelle/jEdit
> manual. There are further fine points still to be sorted out.
> 
> 
> When discussing problems, observations, suggustions, etc. the mail
> subject line should be changed to something meaningful (but the release
> candidate number still given in the message body).
> 
> As usual it is important to keep general laws of causality in mind:
> release candidates may still change, but the final release is final.
> Although this is tautological, in the past few releases we've often had
> complaints right after final lift-off, when it was too late.
> 
> So the best time to start testing is now.
> 
> 
>     Makarius
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.