Lines Matching refs:MIN
369 \subsection{The theory {\tt MIN}}
372 The {\it minimal theory\/}\index{MIN@\ml{MIN}}\index{minimal theory, of HOL logic@minimal theory, of \HOL{} logic} \theory{MIN} is defined by:
374 \theory{MIN} =
381 Since the theory \theory{MIN} has a signature consisting only of
385 Although the theory \theory{MIN} contains only the minimal standard
391 In the implementation, the theory \theory{MIN} is given the name
400 structure as \theory{MIN}. Its signature contains the constants in
401 \theory{MIN} and the following constants:
489 Finally, as for the theory \theory{MIN}, the set ${\sf
494 original theory \theory{MIN}. (The mechanism for making such
507 The unique standard model {\em Min\/} of \theory{MIN} gives rise to a
795 the theory \theory{MIN} in Section~\ref{LOG}. Thus with the notation
798 \theory{LOG}\; =\; \theory{MIN}\;\begin{array}[t]{@{}l}