Re: [isabelle] full proofs



Sean McLaughlin wrote:
> I set
>  proofs:= 2
> in
> Pure/ROOT.ML
> and rebuilt the heap, but this didn't help either
> 
> Any suggestions?

Hello Sean,

changing the value of "proofs" in Pure/ROOT.ML does not help, since "proofs"
is set automatically by the "isatool usedir" script invoked by "build".
To turn on proofs for all sessions, add

  ISABELLE_USEDIR_OPTIONS="-p 2"

to your local isabelle/etc/settings file (see sections 1.1 and 2.4 of the
Isabelle system manual for more information).

Greetings,
Stefan

-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





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