[isabelle-dev] jedit

Lars Noschinski noschinl at in.tum.de
Tue May 15 09:39:51 CEST 2012


On 15.05.2012 08:35, Brian Huffman wrote:
> 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).

At least when you once discovered the "print_" pattern, auto-completion 
comes to your rescue ;)

   -- Lars



More information about the isabelle-dev mailing list