Manual/Guide/guide.tex

559 \item and the lines between {\small\verb!\THEOREM!} and
560 {\small\verb!\ENDTHEOREM!} are the ascii representation of the theorem in
595 \noindent That is, the string `{\small\verb!\none!}' takes the place of the
632 keyword `{\small\verb!\none!}' is used in the \meta{thyname} field:
688 \item {\small\verb!\DOC!}
689 \item {\small\verb!\TYPE!} (or {\small\verb!\BLTYPE!} and {\small\verb!\ELTYPE!})
690 \item {\small\verb!\SYNOPSIS!}
691 \item {\small\verb!\KEYWORDS!}
692 \item {\small\verb!\LIBRARY!} (present only in library documentation)
693 \item {\small\verb!\DESCRIBE!}
694 \item {\small\verb!\FAILURE!}
695 \item {\small\verb!\EXAMPLE!}
696 \item {\small\verb!\USES!}
697 \item {\small\verb!\COMMENTS!}
698 \item {\small\verb!\SEEALSO!}
699 \item {\small\verb!\ENDDOC!}
710 \noindent\qquad{\small\verb!\DOC!\vsp\meta{name}}
725 `{\small\verb!$!}'.  For example, the \meta{name} field for the tactical
726 {\small\verb!THEN!} should simply be `{\small\verb!THEN!}' and not
727 `{\small\verb!$THEN!}'.  The {\small\verb!\DOC!} line is a required field in
729 {\small\verb!\TYPE!} line.
731 An example {\small\verb!\DOC!} line is shown below:
742 \noindent\qquad{\small\verb!\TYPE!\vsp\verb!{!\meta{name}\vsp\ml{:}\vsp\meta{type}\verb!}!}
758 \ML\ function, it must be preceded by the dollar sign `{\small\verb!$!}'.  For
759 example, the \meta{name} field for the tactical {\small\verb!THEN!} should be
760 `{\small\verb!$THEN!}', not `{\small\verb!THEN!}'.  The {\small\verb!\TYPE!}
762 blank line between it and the line beginning `{\small\verb!\SYNOPSIS!}'.
766 {\small\verb!\BLTYPE!} and {\small\verb!\ELTYPE!} (`begin-long-type' and
770 \noindent\qquad{\small\verb!\BLTYPE!}
775 \par\noindent\qquad{\small\verb!\ELTYPE!}
782 first line. When necessary, {\small\verb!\BLTYPE!} and {\small\verb!\ELTYPE!}
783 should be used in place of {\small\verb!\TYPE!}, and all other conventions
784 associated with {\small\verb!\TYPE!} should be adhered to when using them.
786 An example {\small\verb!\TYPE!} line is shown below:
796 The type quoted in the {\small\verb!\TYPE!} should almost always be precisely
798 abbreviated by the built-in type abbreviations (e.g.\ {\small\verb!conv!}) may
800 the type of {\small\verb!AP_THM!} is shown by the system as
801 {\small\verb!thm -> conv!}, but in this case it is clearer to write
802 {\small\verb!(thm -> term -> thm)!} since {\small\verb!AP_THM!} is not really a
805 If the {\small\verb!\TYPE!} field differs from the type printed by the system,
806 then the fact should be noted in the {\small\verb!\COMMENTS!} field.  Unless
811   \item Appearance of {\small\verb!goal!} when a
812         {\small\verb!term list # term!} has no real
814         proof. A good example is {\small\verb!list_mk_forall!}.
815   \item Appearance of {\small\verb!conv!} when a {\small\verb!term -> thm!} is
817         naturally thought of as a conversion. {\small\verb!ASSUME!} at
821 Most {\small\verb!\TYPE!} fields should agree precisely with the system
823 {\small\verb!bin/typecheck!} may therefore be used
847 The {\small\verb!\SYNOPSIS!} field follows the blank line after the
849 consists of a line containing only the keyword `{\small\verb!\SYNOPSIS!}',
852 following the line beginning `{\small\verb!\SYNOPSIS!}'.  There must be
869 An example {\small\verb!\SYNOPSIS!} field for the tactic
870 {\small\verb!ACCEPT_TAC!} is shown below:
911 The {\small\verb!\DESCRIBE!} field consists of a line containing only the
912 keyword `{\small\verb!\DESCRIBE!}', followed by a full description of the
913 \ML\ identifier being documented. The {\small\verb!\DESCRIBE!} field is
916 {\small\verb!\SYNOPSIS!} field.  The text of the description should start on
918 `{\small\verb!\DESCRIBE!}'.  There must be exactly one blank line between
922 The aim of the {\small\verb!\DESCRIBE!} field is to give a complete and
927 used (these belong under {\small\verb!\EXAMPLES!}). Neither should the
929 question (this belongs under {\small\verb!\USES!}).  Comments of a general
931 belong under {\small\verb!\COMMENTS!}.  Failure may be mentioned when it plays
934 {\small\verb!REPEAT!} and {\small\verb!ORELSE!}).  But a description of
936 {\small\verb!dest_comb!} to a variable) does not belong here; this information
937 should instead be given in the {\small\verb!\FAILURE!} field.
939 As an example, here is the {\small\verb!\DESCRIBE!} field for
940 {\small\verb!ACCEPT_TAC!}:
952 \noindent The use of the braces `{\small\verb!{!}' and  `{\small\verb!}!}' in
957 The {\small\verb!\FAILURE!} field consists of a line containing only the
958 keyword `{\small\verb!\FAILURE!}', followed by a full (English language)
960 identifier being documented is used.  The {\small\verb!\FAILURE!} field is
963 beginning `{\small\verb!\FAILURE!}'.  There must be exactly one blank line
967 The {\small\verb!\FAILURE!} field should describe the conditions under which
970 first argument to the function {\small\verb!INDUCT_THEN!} should be a theorem
972 {\small\verb!prove_induction_thm!}.  If the supplied theorem does {\it not\/}
973 have this form, {\small\verb!INDUCT_THEN!} will almost certainly fail.  It is,
974 however, a feature of the way {\small\verb!INDUCT_THEN!} is implemented that
977 {\small\verb!prove_induction_thm!} (users should not depend on this).  The
978 {\small\verb!\FAILURE!} field for {\small\verb!INDUCT_THEN!} should make this
983 Here is an example {\small\verb!\FAILURE!} field for
984 {\small\verb!ACCEPT_TAC!}:
996 \noindent The use of the braces `{\small\verb!{!}' and  `{\small\verb!}!}' in
1001 The {\small\verb!\EXAMPLE!} field consists of a line containing only the
1002 keyword `{\small\verb!\EXAMPLE!}', followed by an illustrative example or
1005 `{\small\verb!\EXAMPLE!}'.  There must be exactly one blank line between the
1009 The {\small\verb!\EXAMPLE!} field is optional, and should be present only when
1039 The {\small\verb!\USES!} field consists of a line containing only the keyword
1040 `{\small\verb!\USES!}', followed by a statement of common or typical uses of
1042 the line immediately following the line beginning `{\small\verb!\USES!}'.
1047 The {\small\verb!\USES!} field is optional, and is likely to be present only
1049 cases, the {\small\verb!\SYNOPSIS!} will already have said everything that
1050 needs to be said about the uses of a function.  A {\small\verb!\USES!} field
1051 will not be needed in these cases.  The {\small\verb!\USES!} field should not
1054 {\small\verb!\SYNOPSIS!} for {\small\verb!SPEC!} is:
1066 \noindent In this case, the {\small\verb!\USES!} field should {\it not\/} be
1079 {\small\verb!\USES!} field for {\small\verb!SPEC!} should be something like:
1091 \noindent But, in the case of {\small\verb!SPEC!}, no {\small\verb!\USES!}
1093 still a paraphrase of the function of {\small\verb!SPEC!}; the second
1094 `use' is rather specific, and using {\small\verb!SPEC!} is only a very small
1099 The {\small\verb!\COMMENTS!} field consists of a line containing only the
1100 keyword `{\small\verb!\COMMENTS!}', followed by any general remarks about the
1103 following the line beginning `{\small\verb!\COMMENTS!}'.  There must be
1108 The {\small\verb!\COMMENTS!} field is optional, and should be used for general
1110 style (e.g.\ `don't use it' in the entry on {\small\verb!POP_ASSUM!}), and so
1120 The {\small\verb!\SEEALSO!} field consists of a line containing only the
1121 keyword `{\small\verb!\SEEALSO!}', followed by list of manual entries
1124 `{\small\verb!\EXAMPLE!}'.  The list itself should consist of a sequence of
1130 When deciding whether to add a cross-reference to the {\verb!SEEALSO!} field,
1134 Here is a sample {\small\verb!\SEEALSO!} field for
1135 {\small\verb!REWRITE_TAC!}:
1150 The {\small\verb!\ENDDOC!} line, which consists of a single line containing
1151 only the keyword `{\small\verb!\ENDDOC!}', signals the end of a manual entry.
1156 The {\small\verb!\SYNOPSIS!}, {\small\verb!\DESCRIBE!},
1157 {\small\verb!\FAILURE!}, {\small\verb!\EXAMPLE!}, {\small\verb!\USES!}, and
1158 {\small\verb!\COMMENTS!} fields of a \doc\ file all consist of a keyword line
1160 command are allowed: `{\small\verb%\noindent%}\vsp' at the beginning of a line,
1161 and {\small\verb%{%}\meta{text}{\small\verb%}%}. These are interpreted as
1165 \item  `{\small\verb%\noindent%}\vsp' at the beginning of a line prevents
1168 \item  An inline {\small\verb%{%}\meta{text}{\small\verb%}%} results in
1170 `{\small\verb%{%}\meta{text}{\small\verb%}%}' is converted to
1171 `{\small\verb!{\small\verb%!}\meta{text}{\small\verb!%}!}'. This means that
1172 \meta{text} should not contain the character `{\small\verb!%!}'.
1174 \item A sequence of lines of the following form, where `{\small\verb|{|}' and
1175 `{\small\verb|}|}' occur at the beginning of otherwise empty lines:
1178   \verb!{!
1180   \verb!}!
1188 `{\small\verb|{|}' and `{\small\verb|}|}' should be manually indented by three
1190 of text and the open bracket `{\small\verb|{|}' and no blank line between the
1191 closing bracket `{\small\verb|}|}' and the following line of text (even if
1350 the rule line should be restated (see the example of {\small\verb!AP_THM!}
1426 Here is a sample \doc\ file for {\small\verb!ACCEPT_TAC!}:
1473 Here is the typeset documentation for the {\small\verb!ACCEPT_TAC!} \doc\ file
1478 \TYPE {\small\verb%ACCEPT_TAC : thm_tactic%}\egroup
1484 {\small\verb%ACCEPT_TAC%} maps a given theorem {\small\verb%th%} to a tactic that solves any goal whose
1485 conclusion is alpha-convertible to the conclusion of {\small\verb%th%}.
1488 {\small\verb%ACCEPT_TAC th (A,g)%} fails if the term {\small\verb%g%} is not alpha-convertible to the
1489 conclusion of the supplied theorem {\small\verb%th%}.
1492 {\small\verb%ACCEPT_TAC%} applied to the axiom