[isabelle] Running Isabelle in batch mode



Hello,

I have noticed that when running Isabelle in batch mode
to check a theory somethings are printed while other
are not.

For example class declarations are printed, but definitions
and theorems are not. However when using

thm SomeFact

then the theorem is printed also.

Is there a way to suppress all outputs from processing
the theory, but still have the output from explicit
writeln inside Isabelle/ML blocks.

Moreover, is it possible to turn this output on and off
from within a theory?

Best regards,

Viorel Preoteasa







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