src/Tools/Code/code_target.ML
changeset 38908 732149f6ebf9
parent 38863 9070a7c356c9
child 38909 919c924067f3
equal deleted inserted replaced
38868:0f861635949d 38908:732149f6ebf9
     1 (*  Title:      Tools/Code/code_target.ML
     1 (*  Title:      Tools/Code/code_target.ML
     2     Author:     Florian Haftmann, TU Muenchen
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     3 
     4 Serializer from intermediate language ("Thin-gol") to target languages.
     4 Generic infrastructure for serializers from intermediate language ("Thin-gol") to target languages.
     5 *)
     5 *)
     6 
     6 
     7 signature CODE_TARGET =
     7 signature CODE_TARGET =
     8 sig
     8 sig
     9   val cert_tyco: theory -> string -> string
     9   val cert_tyco: theory -> string -> string