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). But then the real question is, how do we expect new users to discover this feature? - Brian