Re: [isabelle] add_assoc, add.assoc and reflection
Thank you for the explanations
Name spaces are strictly separate for each "kind" of things. The
syntax is usually done in a way that the distinction of kinds is clear
from how the text is written. E.g. fact expressions refer to
attributes and theorems in a certain way, and cannot be mistaken as
terms, for example.
So I suppose the answer to your question is: theorem names /can/ occur
in inner syntax, but then they do not refer to theorems;
while with respect to the following
The main meta-problem on this thread might be actually an expectation
of something complicated, but the situation is quite plain and
simple. And after decades of reforms of the system implementation it
should all work out smoothly, including arbitrary nesting of languages.
some smoothness is lost in case one uses Isabelle not anticipated by
design, for instance Lucas-Interpretation : Here programs  contain
theorem names, which are turned into theorems by functions available in
Isabelle; this now requires additional conversion .
So thanks a lot for all the replies -- they tell us about prospects on
 We plan to employ Isabelle's function package for that purpose.
This archive was generated by a fusion of
Pipermail (Mailman edition) and