[isabelle-dev] Isabelle gets stuck when imported theory is not found

Christian Sternagel c.sternagel at gmail.com
Thu Mar 5 12:56:11 CET 2015

Just for the record. I think I experienced something similar:




On 03/05/2015 11:39 AM, Johannes Hölzl wrote:
> In rev 304ee0a475d1 I fixed a problem that only appears when one loads
> ~~/src/HOL/Probability interactively based on the HOL image.
> In Measure_Space the theory "Multivariate_Analysis" was imported without
> the correct path. When started with "-l HOL-Multivariate_Analysis" it
> worked.
> Unfortunately there is no error message, it just looks like
> Isabelle/jEdit gets stuck at this point.
> Is there a way to show an error message at the position of the import
> header?
>   - Johannes
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list