[isabelle-dev] jedit

2012-05-15 Thread Tobias Nipkow 
How can I see the possible cases in an induction, i.e. Show me cases in PG?

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

Re: [isabelle-dev] jedit

2012-05-15 Thread Brian Huffman 
On Tue, May 15, 2012 at 8:18 AM, Tobias Nipkow nip...@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).

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

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

Re: [isabelle-dev] jedit

2012-05-15 Thread Tobias Nipkow 
Am 15/05/2012 08:35, schrieb Brian Huffman:
 On Tue, May 15, 2012 at 8:18 AM, Tobias Nipkow nip...@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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] jedit

2012-05-15 Thread Lars Noschinski 

On 15.05.2012 08:35, Brian Huffman wrote:

On Tue, May 15, 2012 at 8:18 AM, Tobias Nipkownip...@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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev