choose_must:(MQGTypes.r_obj list list ->
MQGTypes.r_obj list ->
MQGTypes.r_obj list) ->
- unit -> status: ProofEngineTypes.status -> string list
+ unit -> ProofEngineTypes.status -> string list
(* TODO: OLD CODE TO BE REMOVED
-val searchTheorem : status: ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list
+val searchTheorem : ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list
*)
-val searchTheorems : MQIConn.handle -> status: ProofEngineTypes.status -> (ProofEngineTypes.proof * ProofEngineTypes.goal list) list
-
+val searchTheorems:
+ MQIConn.handle -> ProofEngineTypes.status ->
+ (ProofEngineTypes.proof * ProofEngineTypes.goal list) list