search

andriusvelykis / isabelle-eclipse

Eclipse integration for Isabelle proof assistant.
http://andriusvelykis.github.io/isabelle-eclipse
Eclipse Public License 1.0
12 stars 4 forks source link

View for lemma definitions #83

Open andriusvelykis opened 10 years ago

andriusvelykis commented 10 years ago

Would be nice to lookup lemma definitions for lemmas used in the proof, e.g. similarly to a JavaDoc view in Eclipse for Java.

While this information is likely not available on the client side, it would be nice to query Isabelle in a low-priority process to produce the necessary definition.

andriusvelykis commented 10 years ago

See also discussion in isabelle-users.