exported cert_tyco, read_tyco
authorhaftmann
Wed, 28 Apr 2010 15:17:13 +0200
changeset 36471 5aae37575885
parent 36470 ed9be131a4ec
child 36472 3e677ca1e564
exported cert_tyco, read_tyco
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