# HG changeset patch
# User mengj
# Date 1130459341 -7200
# Node ID 2aecb2d68c00c1cbdc220d68ff49a89373f1312d
# Parent  35ec4681d38f3062f3ef41acf3ce6fc44ef6f5d5
Added "writeln_strs" to the signature

diff -r 35ec4681d38f -r 2aecb2d68c00 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Fri Oct 28 02:28:20 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML	Fri Oct 28 02:29:01 2005 +0200
@@ -13,6 +13,7 @@
   val helper_path: string -> string -> string
   val problem_name: string ref
   val time_limit: int ref
+  val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit
 end;
 
 structure ResAtp: RES_ATP =