Clarified documentation of par-or tactic.

Relates to #269.

src/api/dotnet/Context.cs

@@ -3208,7 +3208,7 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Create a tactic that applies the given tactics in parallel.
+        /// Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).
         /// </summary>
         public Tactic ParOr(params Tactic[] t)
         {

src/api/java/Context.java

@@ -2563,7 +2563,7 @@ public class Context extends IDisposable
     }
 
     /**
-     * Create a tactic that applies the given tactics in parallel.
+     * Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).
      **/
     public Tactic parOr(Tactic... t)
     {

src/api/ml/z3.mli

@@ -2941,7 +2941,7 @@ sig
       Alias for [UsingParams]*)
   val with_ : context -> tactic -> Params.params -> tactic
 
-  (** Create a tactic that applies the given tactics in parallel. *)
+  (** Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail). *)
   val par_or : context -> tactic list -> tactic
 
   (** Create a tactic that applies a tactic to a given goal and then another tactic

src/cmd_context/tactic_cmds.cpp

@@ -94,8 +94,8 @@ void help_tactic(cmd_context & ctx) {
     std::ostringstream buf;
     buf << "combinators:\n";
     buf << "- (and-then <tactic>+) executes the given tactics sequencially.\n";
-    buf << "- (or-else <tactic>+) tries the given tactics in sequence until one of them succeeds.\n";
-    buf << "- (par-or <tactic>+) executes the given tactics in parallel until one of them succeeds.\n";
+    buf << "- (or-else <tactic>+) tries the given tactics in sequence until one of them succeeds (i.e., the first that doesn't fail).\n";
+    buf << "- (par-or <tactic>+) executes the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).\n";
     buf << "- (par-then <tactic1> <tactic2>) executes tactic1 and then tactic2 to every subgoal produced by tactic1. All subgoals are processed in parallel.\n";
     buf << "- (try-for <tactic> <num>) excutes the given tactic for at most <num> milliseconds, it fails if the execution takes more than <num> milliseconds.\n";
     buf << "- (if <probe> <tactic> <tactic>) if <probe> evaluates to true, then execute the first tactic. Otherwise execute the second.\n";