Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: Sean McLaughlin <seanmcl@cmu.edu>
Hi,
I'm trying to get a proof term for sylow_thm.
I tried "build -m HOL-Algebra HOL", which
compiled a heap, but didn't produce proofs apparently:
theory Tmp = Main + Sylow:
thm sylow_thm
full_prf sylow_thm
*** reconstruct_proof: minimal proof object
*** At command "full_prf".
I set
proofs:= 2
in
Pure/ROOT.ML
and rebuilt the heap, but this didn't help either
Any suggestions?
Thanks,
Sean
Email Gateway (Aug 17 2022 at 13:27):From: Stefan Berghofer <berghofe@in.tum.de>
Sean McLaughlin wrote:
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
Last updated: May 03 2024 at 04:19 UTC