Hi Florian,
Anyway, I am not so much concerned about syntax. My primary intention
is to get rid of the experimental code in interpretation_with_defs.ML,
according to the following agenda:
a) Decide for a particular syntax (at the moment this can only be (*) as
it is conservative)
b) Enhance
Quoting Makarius makar...@sketis.net:
It means that a constant c that depends on context parameters x y
z is turned into a fountational constant loc.c in the background,
and then re-imported into the local context as loc.c x y z. Later
it might get re-interpreted such that its dependency
