Table of Contents

Editor

Here you'll find useful information on how to use and configure the editor that comes with iH: the General.

  1. To run a certain program, just press C-c C-n and it will just start from the beginning. To advance one statement, press C-c C-n again. To go one step before, press C-c C-u

Editor Configuration

  1. Is useful when executing, to set the editor to the 3 pane view. On the last version of the General, you can achieve this via Proof-General > Options > Display > Use Three Panes
  2. If you are used to the normal copy and paste shortcuts from other editors, you can enable them in the options menu Options > C-x/C-c/C-v Cut and Paste (CUA). Be sure to then also save your config using Options > Save Options.
  3. You might also want to change the color your theory has when it is accepted by Isabelle/HOL. To do this go to Proof-General > Advanced > Customize > Proof Faces > Proof Locked Face. There you can change the color under Background and then save it using Save for future sessions.