Re: [isabelle] A course based on Isabelle/HOL and some feedback...
Le 26/04/12 17:21, Makarius a écrit :
But the actual scoping is already represented quite nicely in current
Isabelle2011-1 right now, if you use Isabelle/jEdit and rely in its
"Haribo effect". This means the sources are painted in funny colors
according to the role of identifiers. The Prover IDE also has the magic
CONTROL (or COMMAND) key, which asks the system to explain the formal
status of some piece of source.
I just played a bit with both the "Haribo effect" and the "magic"
COMMAND key that are both very nice functionnalities! I will consider
switching to jEdit. Can you tell me if the behavior of jEdit with
nitpick has been improved?
Thanks in advance,
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
This archive was generated by a fusion of
Pipermail (Mailman edition) and