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
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
*** 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
