[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