Re: [isabelle-dev] NEWS: proof outline with cases

2016-08-09 Thread Makarius
On 08/08/16 10:52, Andreas Lochbihler wrote: > 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

Re: [isabelle-dev] NEWS: proof outline with cases

2016-08-08 Thread Andreas Lochbihler
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