...Theory% latex2html id marker 3373 \setcounter{footnote}{1}\fnsymbol{footnote}
Work supported in part by NSF grant CCR-9244739 and ONR contract N00014-92-J-1764. 
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
...already.
Let us assume that the type Proof exists and it represents $proo\!f$. Then a justification could be a function     $t\in$ Sequent $\rightarrow$ Proof. 
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
...Term.% latex2html id marker 3820 \setcounter{footnote}{3}\fnsymbol{footnote}
In a system like HOL based on Standard ML, say SML/HOL, these issues don't arise. In this system, the tactics are not part of the logic. 
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Karla Consroe
5/13/1998