[isabelle-dev] jedit

[Makarius]

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 
statis.

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 
documentation.


 	Makarius