[isabelle-dev] Changes to the locale syntax

Makarius makarius at sketis.net
Sat Nov 14 16:49:55 CET 2015


On Fri, 30 Oct 2015, Makarius wrote:

> I don't mind to change that, and thus make it more uniform.  It is 
> mainly a matter of the empirical situation found in the visible universe 
> of Isabelle examples + AFP if it is feasible / desirable.

To conclude this thread, here are more changes to push it all through.

changeset:   61605:1bf7b186542e
user:        wenzelm
date:        Mon Nov 09 15:48:17 2015 +0100
description:
qualifier is mandatory by default;

changeset:   61606:6d5213bd9709
user:        wenzelm
date:        Mon Nov 09 21:04:49 2015 +0100
description:
uniform mandatory qualifier for all locale expressions, including 
'statespace' parent;
removed obsolete '!' syntax;


Also AFP:

changeset:   5816:f4bb86b97441
user:        wenzelm
date:        Mon Nov 09 20:50:29 2015 +0100
description:
qualifier is mandatory by default;


 	Makarius



More information about the isabelle-dev mailing list