Viewing and Editing Structured Proofs

Contents
  Viewing proofs
  Editing proofs

Viewing Proofs

When you open in the module editor a module containing a theorem wth a proof, you will see a  (-)  next to the theorem and next to each step that has a subproof.  To avoid repeatedly saying step or theorem, we here take a step to be either a theorem or a step of a theorem's proof.  Clicking on the  (-)  next to a step hides the step's proof and changes the  (-)  to a  (+) . Clicking on the  (+)  undoes the effect of clicking on the  (-) .

Right-clicking on a step provides a menu with a section containing the following commands for hiding and revealing parts of the proof of the step at which the cursor is positioned.  These commands can also be executed with the indicated pair of keystrokes.  If you just type Ctl+G (the first keystroke) and wait a second, you will see a list of all the commands telling you what keystroke you should type next.

Show Current Subtree     Ctl+G Ctl+S
Reveals the proof of the step.

Hide Current Subtree     Ctl+G Ctl+H
Hides the proof of the step.

Show Children Only     Ctl+G Ctl+C
Reveals the top level of the step's proof.

Focus on Step     Ctl+G Ctl+F
Hides everything except the top level of the step's proof and the siblings (steps at the same level as) of the step and of every ancestor of that step in the proof.
The following commands can be performed by right-clicking anywhere in the module.
Show All Proofs     Ctl+G Ctl+A
Reveals the complete proof of every theorem in the module.

Hide All Proofs     Ctl+G Ctl+N
Hides the proof of every theorem in the module.
The Focus on Step command performed outside a proof is equivalent to Hide All Proofs

Editing Proofs

There is currently only a single command especially for editing proofs:
Renumber Proof     Ctl+G Ctl+R
A proof step is either named or unnamed.  An unnamed step begins with just a level number, like <4>.  A named step begins with a level number and a name, like <4>7 or <4>xy2 (optionally followed by a period).  Putting the cursor on a proof step and executing the Renumber Proof command causes all the named top-level steps of its proof to be renamed with consecutive numbers, like <4>1, <4>2, etc.
The Toolbox editor's block-selection mode can help in formatting proofs.  We would like to create additional editor commands to make it easier to write and edit proofs, but we don't know what commands would be useful.  Please tell us what commands you would like. 


↑ Proofs