(in-theory <theory> [<implementation>]
[:create-p <create-p>])
Changes the current default theory to the one indicated by <theory> and <implementation>.
<theory> may be any type acceptable to FIND-THEORY. If it is not a theory object, <implementation> will be examined to determine which implementation of the specified theory should be made current. <implementation> should be a symbol (usually a keyword); if unspecified, the current implementation is assumed (see IN-IMPLEMENTATION.)
:CREATE-P - The action taken if appropriate theory does not exist depends on the :CREATE-P keyword argument. If :CREATE-P not supplied or supplied and nil, then an error is signalled. If :CREATE-P is supplied and non-nil, an appropriate theory is instantiated. If CREATE-P is :QUERY (the default), the user will be queried before any such instantiation takes place.
Unlike IN-PACKAGE, an IN-THEORY form at top level in a file side-effects only the load environment (with the possible exception of theory instantiation, as described above.) See also ONTO-LOAD.