Order of material in the file

 

1.

The file header.

2.

Opening comment explaining what the file is and any relevant background material. For long files it may well be useful to include a table of contents.

3.

Opening declarations.

4.

Node definitions - normally presented with the top of the inheritance tree at the top, and the leaves at the bottom.

5.

Closing declarations.

6.

The RCS Id comment.

You should also include, within a comment, some examples of typical theorems that can be derived from the theory: these will help users to see what the ``sensible'' queries are (which may not otherwise be obvious, especially if theorem dump declarations are not included). These example theorems can be included in the opening comment or immediately prior to the closing declarations.