Re: [isabelle] Announcing I3P

Dear all,

I've installed i3p and I've been using it for a few days, so it may be that
my appreciations are not that accurate, but just a few comments:

1. First I would like to emphasize the ease of use of the tool. It
took me no time to install it and in a couple of minutes I was already
writting code (from any point of view much easier than learning emacs
or xemacs for a newbie), and I could install the Isabelle fonts just
following the instructions.

2. I think it is quite fast starting and loading theories and images.

There are also a few things that i did not get to work and I missed from xemacs:

1. I do not know how to switch between the different windows from the
application. For instance, when I'm writting down a theory I would
like to move from the file to the "Result window" to copy the goals or
some of the premises and take them back to the "thy" file. I did not
manage to do it. This feature would ease faster development.

2. X-symbols are not displayed in my files (but they are in the
"Result prover" window). Whenever I write "\<And>" or any other symbol
i3p does not automatically convert it into its X-symbol version. Can
this option be turned on from any menu?

3. There is not keyboard shortcut for the "Isabelle" menu. By means of
"Alt + e" or "Alt + t" one can move to the Edit or Tools menu, but
there is no such option for the "Isabelle" menu.

4. I could not find any mail address inside of the application to
which one could send any congratulations :-)) comments, questions or

Alltogether, I found it really nice and very convenient for starters,
and with minor improvements better than the emacs or xemacs options.

Congratulations to Holger,

best wishes,


Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at ; web:
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.