out: Dumping Theories to Files

$$\mbox{{\tt out($F$)}}$$

Saves the current theory in its current perhaps only partially saturated form, including the ordering definition, into file $F$. The saved file can be used as a theory module in in and add commands as well as in use directives, cf. add. If the module is part of a theory that is to be saturated, no inferences will be computed in which all premises are clauses of the theory module.

Warning: even if the theory is not fully saturated upon saving, later re-uses of the theory might not consider all inferences between theory clauses.

Imprint | Data Protection