[isabelle] using oops in document preparation



Hi,

 

I have

 

lemma "¬ False"

proof (simp only:  ) (*<*) oops  (*>*)

 

which leads to the

 

   Failed to apply initial proof method

 

error message in the interactive development. 

 

oops recovers from the error and I can write other theorem statements.

 

The Isabelle/Isar reference manual writes:

 

A typical application of oops is to explain Isar proofs within the system
itself,

in conjunction with the document preparation tools of Isabelle described in

chapter 4. Thus partial or even wrong proof attempts can be discussed in a

logically sound manner. Note that the Isabelle LaTeX macros can be easily

adapted to print something like ?...? instead of the keyword ?oops?.

 

When I use

 

   isabelle build ?D .

 

I get the same error as above and no output is produced.

 

I tried ?o quick_and_dirty but in vain.

 

How can I include failed proof attempts into a proof document?

 

I use Isabelle2016.

 

- Gergely

 

 




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