If the user has asked to Specify prover usage of Spec axioms/theorems earlier, a menu Specify theorem usage as default in Spec will appear. For each axiom in the axiom list, the user will be asked to select one or more options from the list
Rewrite Forward Backward Left-to-Right Right-to-Left Ignore.
The meaning of these options is given in the section Specify
Proof Directives
(
).
This concludes the discussion of the theorem-proving options made available by clicking Customize on the top menu bar. The consequences of these choices will be made apparent in the discussion of the examples. We now discuss another item that can be selected from the top menu bar, Prover Options.