The Theorems window contains the answers to queries in the global context of the Coq proof assistant. Thus, everytime you send a Search, Check, Eval, or Compute command to Coq (see the keyboard accelerators to know easy ways to send such commands), the result is displayed in this window.

It is possible to set aside the contents of this window by typing <Shift>-D while the mouse is in there. This opens a new Library Fragment window with the contents of the Theorems window in it.

Otherwise, the theorems window enjoys the same properties as the State window. In particular, proof-by-pointing and other advanced editing tools are provided. When using proof-by-pointing, the system has to decide for what goal the command should be generated. It is always the current goal, as indicated by the rank in the tool bar. Proof-by-pointing refuses to work if there is no goal in the State window.

Library Windows

The way it is organized, the Theorems window looses its contents at every new Search or Check request. A simple way to avoid data being overwritten at the next request is to save it in another window. This is what Library windows are for. You can obtain a new Library window by type <Shift>-D while the mouse is in the Theorems window. For use in proof-by-pointing, Library windows serve exactly the same purpose as the Theorems window. A notable asset is also that you can edit their contents.This is useful if you have a collection of theorems that you use very often. You can copy and paste these theorems to group them in one window that will keep these theorems at hand. You can even save such a "menu" of frequently used theorems in a polish format. You will then be able to use this menu in several working session, or adapt your working environment to a specific domain by loading the relevant collection of theorems in the interface.