Manual/Guide/guide.tex

64 beginning sections of this note useful when they wish to typeset the \HOL\
576 \noindent The meaning of this theorem is clear only when it is known that
581 There are certain theorems which  are bound to \ML\ identifiers when the
597 theorems which are bound to \ML\ identifiers when a library is loaded, but
784 associated with {\small\verb!\TYPE!} should be adhered to when using them.
811   \item Appearance of {\small\verb!goal!} when a
815   \item Appearance of {\small\verb!conv!} when a {\small\verb!term -> thm!} is
885 when you cannot remember the name, but do know the kind of thing you are
914 almost always a required field; it is omitted only when the item being
931 belong under {\small\verb!\COMMENTS!}.  Failure may be mentioned when it plays
932 a role in the function's behaviour when applied to arguments for which it is
933 intended (e.g.\ when failure is used for backtracking, as in
959 specification of the conditions under which evaluation can fail when the \ML\
961 required, even when the function being described cannot fail.  The text of the
975 this function may succeed, and even do the intended thing, when supplied with
979 clear, perhaps by stating that this function succeeds when applied to theorems
1009 The {\small\verb!\EXAMPLE!} field is optional, and should be present only when
1012 code displayed (see section~\ref{typesetting}) when necessary. Examples should
1203 solve the current goal.  This kind of tactic is very useful when dealing with
1213 text by three spaces: when an example is presented without accompanying
1286 \noindent Assumption lists of goals should be shown, even when they do not play
1301 deemed to be the same when taking the union.  If this is an important