[isabelle-dev] NEWS: proof outline with cases

Makarius makarius at sketis.net
Sat Jul 16 13:14:09 CEST 2016

Previous message (by thread): [isabelle-dev] \nexists
Next message (by thread): [isabelle-dev] Broken AFP
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

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

Previous message (by thread): [isabelle-dev] \nexists
Next message (by thread): [isabelle-dev] Broken AFP
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the isabelle-dev mailing list