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

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,

Jesus

--
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 unirioja.es ; web: http://www.unirioja.es/cu/jearansa
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.