[isabelle] Feature request: definition on crtl+hover
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?
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