- (* boolean value: true = in main position *)
- choose_must:((MQGTypes.uri * bool) list list ->
- (MQGTypes.uri * bool) list ->
- (MQGTypes.uri * bool) list) ->
- unit -> status: ProofEngineTypes.status -> string list
+ choose_must:(MQGTypes.r_obj list list ->
+ MQGTypes.r_obj list ->
+ MQGTypes.r_obj list) ->
+ unit -> ProofEngineTypes.status -> string list
+
+
+(* TODO: OLD CODE TO BE REMOVED
+val searchTheorem : ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list
+*)
+
+val searchTheorems:
+ MQIConn.handle -> ProofEngineTypes.status ->
+ (ProofEngineTypes.proof * ProofEngineTypes.goal list) list