# 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.
`

and

`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 [1]: Here programs [2] contain
``theorem names, which are turned into theorems by functions available in
``Isabelle; this now requires additional conversion [3].
`

`So thanks a lot for all the replies -- they tell us about prospects on
``Eisbach.
`
Walther
[1] http://eptcs.web.cse.unsw.edu.au/paper.cgi?THedu11.5
[2] We plan to employ Isabelle's function package for that purpose.
[3] https://intra.ist.tugraz.at/hg/isa/rev/419308245588

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*