[isabelle-dev] NEWS: proof outline with cases

Makarius makarius at sketis.net
Tue Aug 9 23:36:19 CEST 2016


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 3_2).

See now

changeset:   63640:c273583f0203
parent:      63633:4302f86920fe
user:        wenzelm
date:        Tue Aug 09 19:44:28 2016 +0200
files:       src/Pure/Isar/proof_context.ML src/Pure/Isar/token.ML
description:
print name in parsable form;


	Makarius




More information about the isabelle-dev mailing list