[isabelle-dev] Suppress odd .prv files
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.
>> 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.
More information about the isabelle-dev