# HG changeset patch
# User wenzelm
# Date 1636481867 -3600
# Node ID d14918fcbd3787c88db40a6ae847831802929046
# Parent  a06652d397a7f811b50721545b27383811b959f3
tuned text;

diff -r a06652d397a7 -r d14918fcbd37 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Tue Nov 09 17:20:04 2021 +0100
+++ b/src/HOL/SMT.thy	Tue Nov 09 19:17:47 2021 +0100
@@ -736,7 +736,7 @@
 
 text \<open>
 The option \<open>smt_read_only_certificates\<close> controls whether only
-stored certificates are should be used or invocation of an SMT solver
+stored certificates should be used or invocation of an SMT solver
 is allowed. When set to \<open>true\<close>, no SMT solver will ever be
 invoked and only the existing certificates found in the configured
 cache are used;  when set to \<open>false\<close> and there is no cached