B.1.6 option: Set System Option

B.1.6 option: Set System Option

Synopsis

Alternative Applications

• Window Menu "Options", Item "No Automatic Simplification":
  option autosimp="false"
• Window Menu "Options", Item "Automatic Simplification":
  option autosimp="true"

Applicable

In declaration mode and in proving mode.

Description

This command switches on the option named I respectively sets the value of this option. Currently the following option is supported:

autosimp

This option may have the value true (default) or false. Setting the option affects the "simplification mode" of the system: If the option is true, all formulas in all proof states are automatically simplified with the help of an external transformation procedure. If the option is false, no automatic simplification is applied; in this case, the user may invoke the command simplify to explicitly trigger the simplification of selected proof states or formulas. When a new proof is started, the proof is executed in the currently active simplification mode. This mode is recorded in the proof such that the proof may be stored and later continued respectively replayed independently of the simplification mode active at that time. If the command is executed during a proof, a single child state is generated whose simplification mode is set according to the value of the option. Thus different parts of a proof may operate in different simplification modes.

B.1.6 option: Set System Option