# HG changeset patch
# User haftmann
# Date 1272460633 -7200
# Node ID 5aae37575885443b3f791517dc396cb52b2fbeb2
# Parent  ed9be131a4eceb0136611c4c38fe69e88e3c3365
exported cert_tyco, read_tyco

diff -r ed9be131a4ec -r 5aae37575885 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Apr 28 15:17:09 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Wed Apr 28 15:17:13 2010 +0200
@@ -6,6 +6,9 @@
 
 signature CODE_TARGET =
 sig
+  val cert_tyco: theory -> string -> string
+  val read_tyco: theory -> string -> string
+
   type serializer
   type literals = Code_Printer.literals
   val add_target: string * (serializer * literals) -> theory -> theory