# HG changeset patch # User blanchet # Date 1378889829 -7200 # Node ID 1905ebfec3738dc9040df64278eb90e242f08925 # Parent 1165e8960f594ec2125a143746339c2746834e51 updated docs diff -r 1165e8960f59 -r 1905ebfec373 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Wed Sep 11 09:51:30 2013 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Wed Sep 11 10:57:09 2013 +0200 @@ -1098,7 +1098,7 @@ are potentially generated. Whether monomorphization takes place depends on the type encoding used. If the option is set to \textit{smart}, it is set to a value that was empirically found to be appropriate for the prover. For most provers, -this value is 200. +this value is 100. \nopagebreak {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}