val file_of_theory : driver -> string -> Theory.theory -> stringval call_on_buffer :
command:string ->
limit:Call_provers.resource_limit ->
gen_new_file:bool ->
?inplace:bool ->
filename:string ->
printer_mapping:Printer.printer_mapping ->
driver ->
Buffer.t ->
Call_provers.prover_callval print_task :
?old:in_channel ->
driver ->
Format.formatter ->
Task.task ->
unitval print_theory :
?old:in_channel ->
driver ->
Format.formatter ->
Theory.theory ->
unitval prove_task :
command:string ->
limit:Call_provers.resource_limit ->
?old:string ->
?inplace:bool ->
?interactive:bool ->
driver ->
Task.task ->
Call_provers.prover_callval print_task_prepared :
?old:in_channel ->
driver ->
Format.formatter ->
Task.task ->
Printer.printer_mappingval prove_task_prepared :
command:string ->
limit:Call_provers.resource_limit ->
?old:string ->
?inplace:bool ->
?interactive:bool ->
driver ->
Task.task ->
Call_provers.prover_callval syntax_map : driver -> Printer.syntax_map