[isabelle-dev] Isabelle gets stuck when imported theory is not found
makarius at sketis.net
Thu Mar 5 15:17:38 CET 2015
On Thu, 5 Mar 2015, Christian Sternagel wrote:
> Just for the record. I think I experienced something similar:
Thanks for the reminder. I will try to pick up this old thread soon for
the coming release. The problem is a consequence of various
"improvements" done elsewhere. I did not make any attempt to change that
yet, since I have already a better idea to handle the files that are
referenced in theory sources, both imports and ML_files.
Thus we have a chance for a genuine improvement of that aspect in the
coming release. As we are moving towards it in Apr/May 2015, it will need
extra sharp eyes watching out for such fine points.
More information about the isabelle-dev