src/Pure/Tools/codegen_package.ML
changeset 17157 c5fb1fb537c0
parent 17156 e50f95ccde99
child 17158 d68bf267cbba
equal deleted inserted replaced
17156:e50f95ccde99 17157:c5fb1fb537c0
     1 signature CODEGEN_PACKAGE =
       
     2 sig
       
     3 end;
       
     4 
       
     5 structure CodegenPackage : CODEGEN_PACKAGE =
       
     6 struct
       
     7 
       
     8 end;