[isabelle-dev] jedit

Tobias Nipkow nipkow at in.tum.de
Tue May 15 08:40:53 CEST 2012


Am 15/05/2012 08:35, schrieb Brian Huffman:
> On Tue, May 15, 2012 at 8:18 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
>> How can I see the possible cases in an induction, i.e. Show me cases in PG?
> 
> You can type the command "print_cases" into your theory file (this
> also works in PG).

Thanks!

> But then the real question is, how do we expect new users to discover
> this feature?

That is easy: you email the mailing list ;-)

Tobias



More information about the isabelle-dev mailing list