[isabelle-dev] Suppress odd .prv files

Makarius makarius at sketis.net
Wed Mar 25 15:10:38 CET 2015


On Thu, 19 Mar 2015, Larry Paulson wrote:

> Within HOL-SPARK. Example attached.
> Larry
>
>> On 19 Mar 2015, at 15:21, Makarius <makarius at sketis.net> wrote:
>>
>> I've never seen such *.prv files.  Where are they coming from?

In Isabelle/e749a0f2f401 there is now a system option spark_prv, which is 
off for the HOL-SPARK example sessions.

So if you remove your local .prv once, they will not be created again.


 	Makarius


More information about the isabelle-dev mailing list