Re: [isabelle] THY path



You can refer to theories in other AFP entries simply by writing

imports "../other-article-name/theory-name"

This is the standard way of doing it.

Tobias

Christian Sternagel schrieb:
> Hi!
> 
> 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
> 1) HOL-First-Entry
> 2) HOL-First-and-Second-Entry
> 3) HOL-First-and-Second-and-Third-Entry
> 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? ;)
> 
> cheers
> 
> chris





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