[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