[isabelle] THY path
is there a way of telling Isabelle where to search for THY files? From
the error message in PG-Emacs when trying to load a non-existing THY
file, I get that the standard search is "." and
"$ISABELLE_HOME/src/HOL/Library". I would like to extend this list.
The reason is that we have 3 entries in the AFP which our development is
based on (currently we have local copies of the corresponding THY
files). To me, it would seem as an overkill, if I had to incrementally
construct heap images for
and then use 'HOL-First-and-Second-and-Third-Entry instead' of 'HOL'.
What do you think? How do other users that base their work on AFP
entries, handle such situations? Andreas? ;)
This archive was generated by a fusion of
Pipermail (Mailman edition) and