src/Pure/Concurrent/multithreading.ML

 sig
   val max_threads: unit -> int
   val max_threads_update: int -> unit
   val enabled: unit -> bool
   val relevant: 'a list -> bool
+  val parallel_proofs: int ref
+  val parallel_proofs_enabled: int -> bool
   val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
   val trace: int ref
   val tracing: int -> (unit -> string) -> unit
   val tracing_time: bool -> Time.time -> (unit -> string) -> unit
   val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a

 fun enabled () = max_threads () > 1;
 
 val relevant = (fn [] => false | [_] => false | _ => enabled ());
 
 end;
+
+
+(* parallel_proofs *)
+
+val parallel_proofs = ref 1;
+
+fun parallel_proofs_enabled n =
+  enabled () andalso ! parallel_proofs >= n;
 
 
 (* synchronous wait *)
 
 fun sync_wait time cond lock =