Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Document Preparation Proofs in Isabelle 2011-1

view this post on Zulip Email Gateway (Aug 18 2022 at 18:49):

From: Simon Foster <S.Foster@dcs.shef.ac.uk>
Hi,

I've been trying to prepare a latex document in the latest version of Isabelle. I've used isabelle mkdir to create a session and copied in some Isabelle files. It compiles fine, but all the proofs are only shown as <proof>. How can I get the proof output to be shown verbosely?

Thanks,

-Simon Foster.

view this post on Zulip Email Gateway (Aug 18 2022 at 18:49):

From: Makarius <makarius@sketis.net>
This can be controled by isabelle usedir option -V (see also the system
manual section 3.4, page 22). The default is to show proofs, but you
probably have some unexpected ISABELLE_USEDIR_OPTIONS via settings or
IsaMakefile.

Makarius

Last updated: Apr 19 2024 at 01:05 UTC