diff --git a/src/api/dotnet/Probe.cs b/src/api/dotnet/Probe.cs
index c10755263..3c5e5adc9 100644
--- a/src/api/dotnet/Probe.cs
+++ b/src/api/dotnet/Probe.cs
@@ -28,7 +28,7 @@ namespace Microsoft.Z3
     /// which solver and/or preprocessing step will be used.
     /// The complete list of probes may be obtained using the procedures <c>Context.NumProbes</c>
     /// and <c>Context.ProbeNames</c>.
-    /// It may also be obtained using the command <c>(help-tactics)</c> in the SMT 2.0 front-end.
+    /// It may also be obtained using the command <c>(help-tactic)</c> in the SMT 2.0 front-end.
     /// </summary>
     [ContractVerification(true)]
     public class Probe : Z3Object
diff --git a/src/api/dotnet/Tactic.cs b/src/api/dotnet/Tactic.cs
index 8399490d5..0a6f79494 100644
--- a/src/api/dotnet/Tactic.cs
+++ b/src/api/dotnet/Tactic.cs
@@ -26,7 +26,7 @@ namespace Microsoft.Z3
     /// Tactics are the basic building block for creating custom solvers for specific problem domains.
     /// The complete list of tactics may be obtained using <c>Context.NumTactics</c> 
     /// and <c>Context.TacticNames</c>.
-    /// It may also be obtained using the command <c>(help-tactics)</c> in the SMT 2.0 front-end.
+    /// It may also be obtained using the command <c>(help-tactic)</c> in the SMT 2.0 front-end.
     /// </summary>
     [ContractVerification(true)]
     public class Tactic : Z3Object
diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java
index e190229df..625b41e09 100644
--- a/src/api/java/Probe.java
+++ b/src/api/java/Probe.java
@@ -22,7 +22,7 @@ package com.microsoft.z3;
  * may be used to decide which solver and/or preprocessing step will be used.
  * The complete list of probes may be obtained using the procedures
  * {@code Context.NumProbes} and {@code Context.ProbeNames}. It may
- * also be obtained using the command {@code (help-tactics)} in the SMT 2.0
+ * also be obtained using the command {@code (help-tactic)} in the SMT 2.0
  * front-end.
  **/
 public class Probe extends Z3Object
diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java
index 81d886537..786f8a6ec 100644
--- a/src/api/java/Tactic.java
+++ b/src/api/java/Tactic.java
@@ -21,7 +21,7 @@ package com.microsoft.z3;
  * Tactics are the basic building block for creating custom solvers for specific
  * problem domains. The complete list of tactics may be obtained using
  * {@code Context.NumTactics} and {@code Context.TacticNames}. It may
- * also be obtained using the command {@code (help-tactics)} in the SMT 2.0
+ * also be obtained using the command {@code (help-tactic)} in the SMT 2.0
  * front-end.
  **/
 public class Tactic extends Z3Object
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index dba15c85d..02f29d080 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -2779,7 +2779,7 @@ end
     which solver and/or preprocessing step will be used.
     The complete list of probes may be obtained using the procedures [Context.NumProbes]
     and [Context.ProbeNames].
-    It may also be obtained using the command [(help-tactics)] in the SMT 2.0 front-end.
+    It may also be obtained using the command [(help-tactic)] in the SMT 2.0 front-end.
 *)
 module Probe :
 sig
@@ -2841,7 +2841,7 @@ end
     Tactics are the basic building block for creating custom solvers for specific problem domains.
     The complete list of tactics may be obtained using [Context.get_num_tactics] 
     and [Context.get_tactic_names].
-    It may also be obtained using the command [(help-tactics)] in the SMT 2.0 front-end.
+    It may also be obtained using the command [(help-tactic)] in the SMT 2.0 front-end.
 *)
 module Tactic :
 sig
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 2312f4389..d0bf20188 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6650,7 +6650,7 @@ END_MLAPI_EXCLUDE
     /**
        \brief Return a tactic associated with the given name.
        The complete list of tactics may be obtained using the procedures #Z3_get_num_tactics and #Z3_get_tactic_name.
-       It may also be obtained using the command <tt>(help-tactics)</tt> in the SMT 2.0 front-end.
+       It may also be obtained using the command <tt>(help-tactic)</tt> in the SMT 2.0 front-end.
     
        Tactics are the basic building block for creating custom solvers for specific problem domains.
 
@@ -6677,7 +6677,7 @@ END_MLAPI_EXCLUDE
     /**
        \brief Return a probe associated with the given name.
        The complete list of probes may be obtained using the procedures #Z3_get_num_probes and #Z3_get_probe_name.
-       It may also be obtained using the command <tt>(help-tactics)</tt> in the SMT 2.0 front-end.
+       It may also be obtained using the command <tt>(help-tactic)</tt> in the SMT 2.0 front-end.
 
        Probes are used to inspect a goal (aka problem) and collect information that may be used to decide
        which solver and/or preprocessing step will be used.