1\DOC
2
3\TYPE {conv = term -> thm}
4
5\SYNOPSIS
6The type of a function which 
7finds an equal term and returns a theorem stating the equality
8
9\KEYWORDS
10conversion.
11
12\DESCRIBE
13If the function {c} is not only of the right type, 
14but is actually what we call a conversion, then
15{(c : conv) (t : term)} returns a theorem of the form
16{
17   |- t = t'
18}
19If (roughly speaking) {t} is of the right form to be passed to {c},
20but {c} doesn't find a desired equal term {t'}
21then {c t} may raise the exception {UNCHANGED} in preference to returning
22{|- t = t}, as it can be dealt with more efficiently.
23
24\SEEALSO
25Conv.UNCHANGED
26
27\ENDDOC
28
29