[isabelle-dev] NEWS: proof outline with cases

Andreas Lochbihler andreas.lochbihler at inf.ethz.ch
Mon Aug 8 10:52:59 CEST 2016

Hi Makarius,

Just a quick feedback on the proof outlines: they are great! But sometimes quotes are 
needed around the case name (e.g., if it is a keyword like "try" or "oracle", or if it is 
a case of an induction rule by the function package for an equation which has been split 
up by the sequential option, i.e., 3_1 and 3_2). Could you add the missing quotes to the 

(For reference: tested with Isabelle/eca71be9c948)


On 16/07/16 13:14, Makarius wrote:
> *** Prover IDE -- Isabelle/Scala/jEdit ***
> * Command 'proof' provides information about proof outline with cases,
> e.g. for proof methods "cases", "induct", "goal_cases".
> This refers to Isabelle/6c46a1e786da. The main functionality is in
> Isabelle/9f8d06f23c09, which also demonstrates how to do such things
> with existing PIDE infrastructure.
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list