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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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 sequential option, i.e., 3_1 and 3_2). Could you add the missing quotes to the 
outline?


(For reference: tested with Isabelle/eca71be9c948)

Best,
Andreas

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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS: proof outline with cases

2016-07-16 Thread Makarius 
*** 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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev