## Introduction

## General commands (viewing data and setting parameters)

## Proof commands (The 'GumTree' User Interface for Ergo 5 proofs)

## Proof Information Commands

## Proof Tree Commands

## Query Procedures

## Save/Close/Read Proof Commands

## Tactic Combinator Commands

## User Defined Gumtree Tactics

## Theory/Database Commands (The DBMS user interface)

## I/O Syntactic Sugar Commands.

## Miscellaneous Commands.

## Rule/Tactic Table Commands

## User Defined Tactic Tables

## Save/Exit Commands.

## Table Commands

## User Defined Tables

## Tactic File Commands.

## Theory Construction Commands.

## Theory Deletion Commands.

## Theory Extension Commands.

## Parameters

## Concepts

## Annotations on proof nodes

## Constraints on rules

## Modes and Types

## Ergo5 types