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
example.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
