Re: [isabelle] A course based on Isabelle/HOL and some feedback...





Dear Makarius,


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,

Thomas

--
Thomas Genet
ISTIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
http://www.irisa.fr/celtique/genet





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