summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Fri, 26 May 2000 11:17:53 +0200 | |

changeset 8978 | 894d76cbf56d |

parent 8977 | dd8bc754a072 |

child 8979 | 802acc97fdaf |

fixed the documentation of goalw_cterm and prove_goalw_cterm

--- a/doc-src/Ref/goals.tex Thu May 25 15:22:19 2000 +0200 +++ b/doc-src/Ref/goals.tex Fri May 26 11:17:53 2000 +0200 @@ -87,11 +87,10 @@ meta-rewrite rules to the first subgoal and the premises. \index{meta-rewriting} -\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct};] is - a version of \texttt{goalw} for programming applications. The main - goal is supplied as a cterm, not as a string. Typically, the cterm - is created from a term~$t$ by \texttt{cterm_of (sign_of thy) $t$}. - \index{*cterm_of}\index{*sign_of} +\item[\ttindexbold{goalw_cterm} {\it defs} {\it ct};] is + a version of \texttt{goalw} intended for programming. The main + goal is supplied as a cterm, not as a string. See also + \texttt{prove_goalw_cterm}, \S\ref{sec:executing-batch}. \item[\ttindexbold{premises}()] returns the list of meta-hypotheses associated with the current proof (in @@ -482,7 +481,7 @@ \end{ttdescription} -\section{Executing batch proofs} +\section{Executing batch proofs}\label{sec:executing-batch} \index{batch execution}% To save space below, let type \texttt{tacfn} abbreviate \texttt{thm list -> tactic list}, which is the type of a tactical proof. @@ -496,8 +495,9 @@ These batch functions create an initial proof state, then apply a tactic to it, yielding a sequence of final proof states. The head of the sequence is returned, provided it is an instance of the theorem originally proposed. -The forms \texttt{prove_goal}, \texttt{prove_goalw} and \texttt{prove_goalw_cterm} -are analogous to \texttt{goal}, \texttt{goalw} and \texttt{goalw_cterm}. +The forms \texttt{prove_goal}, \texttt{prove_goalw} and +\texttt{prove_goalw_cterm} are analogous to \texttt{goal}, \texttt{goalw} and +\texttt{goalw_cterm}. The tactic is specified by a function from theorem lists to tactic lists. The function is applied to the list of meta-assumptions taken from @@ -536,15 +536,15 @@ \item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;] is analogous to \texttt{qed_goal}. -\item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct} +\item[\ttindexbold{prove_goalw_cterm} {\it defs} {\it ct} {\it tacsf};] -is a version of \texttt{prove_goalw} for programming applications. The main -goal is supplied as a cterm, not as a string. Typically, the cterm is -created from a term~$t$ as follows: +is a version of \texttt{prove_goalw} intended for programming. The main +goal is supplied as a cterm, not as a string. A cterm carries a theory with + it, and can be created from a term~$t$ by \begin{ttbox} -cterm_of (sign_of thy) \(t\) +cterm_of (sign_of thy) \(t\) \end{ttbox} -\index{*cterm_of}\index{*sign_of} + \index{*cterm_of}\index{*sign_of} \end{ttdescription}