[isabelle-dev] Mirabelle and load path

Sascha Boehme boehmes at in.tum.de
Wed Mar 23 10:28:31 CET 2011

Alexander Krauss wrote:
> On 03/22/2011 10:17 PM, Makarius wrote:
> >I also wonder about mirabelle -q, which produces strange messages in the
> >regular makeall setup:
> >
> >http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Mirabelle/lib/scripts/mirabelle.pl#l134
> >
> >http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Mirabelle/lib/scripts/mirabelle.pl#l139
> >
> >
> >Is this really intended, or just due to the confusing ne "" test?

Changeset d3404f32328a silences these two lines.  I'm not quite sure
whether they are necessary at all, but they might come in handy when
running Mirabelle with several theories.


More information about the isabelle-dev mailing list