# HG changeset patch # User blanchet # Date 1338971705 -7200 # Node ID 72b093caf048636e86d63feb82a9ba30fc9b2214 # Parent 25efe19cd4e916a195194e74ab0248a2f68c2088 swap adjectives (cf. Google) diff -r 25efe19cd4e9 -r 72b093caf048 doc-src/Sledgehammer/sledgehammer.tex --- 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]