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