src/HOL/SMT.thy

 Each SMT solver provides several commandline options to tweak its
 behaviour.  They can be passed to the solver by setting the following
 options.
 *}
 
-declare [[ cvc3_options = "", remote_cvc3_options = "" ]]
+declare [[ cvc3_options = "" ]]
 declare [[ yices_options = "" ]]
-declare [[ z3_options = "", remote_z3_options = "" ]]
+declare [[ z3_options = "" ]]
 
 text {*
 Enable the following option to use built-in support for datatypes and
 records.  Currently, this is only implemented for Z3 running in oracle
 mode.