exported cert_tyco, read_tyco
authorhaftmann
Wed Apr 28 15:17:13 2010 +0200 (2010-04-28)
changeset 364715aae37575885
parent 36470 ed9be131a4ec
child 36472 3e677ca1e564
exported cert_tyco, read_tyco
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Wed Apr 28 15:17:09 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Wed Apr 28 15:17:13 2010 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  
     1.5  signature CODE_TARGET =
     1.6  sig
     1.7 +  val cert_tyco: theory -> string -> string
     1.8 +  val read_tyco: theory -> string -> string
     1.9 +
    1.10    type serializer
    1.11    type literals = Code_Printer.literals
    1.12    val add_target: string * (serializer * literals) -> theory -> theory