[isabelle] Feature request: definition on crtl+hover

Dear all,

I would ask that when you ctrl+hover on a function definition 
(such as mysucc in attached hover.thy) then not only the 
typing information of mysucc ("nat => nat") shows up but 
also the body of the function ("mysucc n = n + 1"). Or does that 
feature already exist?

theory hover
imports Main 

definition mysucc::"nat => nat" where "mysucc n = n + 1" 

lemma "mysucc 1 = 2" by (simp add: mysucc_def)   


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