Go to definition

The definitions of most elements in the proof script and proof output (e.g. data types, operators, lemmas, proof commands, etc.) can be accessed via these selections:

• Ctrl + click via the hyperlink (Cmd + click on Mac OS X). Note that you may need to move the mouse and hover over the definition while pressing Ctrl (Cmd) for the hyperlink to appear.

  

• Navigate > Open Definition in the menu, while the cursor is placed on the element (editor only for now).
• F3 keyboard shortcut - same as the menu option above.

The hyperlinks are supported both in Isabelle editor and Prover Output view.

When selected, the definition of target element will be opened and selected in the editor.

Note that definitions in Isabelle ML files may be opened in an external editor if no ML editor is available within Eclipse.