Re: [isabelle] using oops in document preparation



On 12/07/16 09:29, Gergely Buday wrote:
> 
> lemma "¬ False"
> proof (simp only:  ) (*<*) oops  (*>*)
> 
> 
> oops recovers from the error and I can write other theorem statements.
> 
> When I use
> 
>    isabelle build –D .
> 
> I get the same error as above and no output is produced.

Batch build is strict about errors and won't recover.


> How can I include failed proof attempts into a proof document?
> 
> I use Isabelle2016.

I recommend the new document antiquotation @{theory_text} (see also NEWS).


	Makarius






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