| changeset 48078 | 72b093caf048 |
| parent 48006 | 8d989b9c8e4f |
| child 48090 | 433787f8145e |
--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Jun 06 10:35:05 2012 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Jun 06 10:35:05 2012 +0200 @@ -1086,7 +1086,7 @@ monomorphized. \item[\labelitemi] \textbf{\textit{poly\_native} (sound):} Exploits native -polymorphic first-order types if the prover supports the TFF1 syntax; otherwise, +first-order polymorphic types if the prover supports the TFF1 syntax; otherwise, falls back on \textit{mono\_native}. \item[\labelitemi]