makarius at sketis.net
Wed May 16 15:08:25 CEST 2012
On Tue, 15 May 2012, 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).
> But then the real question is, how do we expect new users to discover
> this feature?
>From the fine manual? 'cases' and 'print_cases' are directly adjacent in
the isar-ref manual. The existence of 'print_foo' commands in Isabelle
should not be surprising to any Isabelle user. Historically, Proof
General has offered some of them in the menus, but this was not continued
after its updates stopped following Isabelle releases; and now PG is in
Moreover, the isar-ref manual already has formal markup for almost
everything. So in the next round of refinement, I will probably extend
the existing hyperlink facility in Isabelle/jEdit to point to the
More information about the isabelle-dev