[isabelle-dev] NEWS: Isabelle sessions and build management

Makarius makarius at sketis.net
Mon Jul 30 12:55:02 CEST 2012

On Sun, 29 Jul 2012, Makarius wrote:

> Here is a one-liner for private use in $ISABELLE_HOME_USER/ROOT:
>  session HOL-Test! in "~~/src/HOL" = Pure + theories Nat
> This works because $ISABELLE_HOME_USER is also a component.

Oops, the non-identifier name "HOL-Test" above needs to be quoted, 
according to the usual conventions of Isar outer syntax that is used for 
these config files:

   session "HOL-Test"! in "~~/src/HOL" = Pure + theories Nat

This lapse indicates another future issue, when session names shall be 
used to qualify theory names: we might have to change the global naming 
scheme to make them (long) identifiers without funny dashes.  Otherwise 
the qualification would not be usable within the term language, for 


More information about the isabelle-dev mailing list