doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML
changeset 21178 c3618fc6a6f7
child 21993 4b802a9e0738
equal deleted inserted replaced
21177:e8228486aa03 21178:c3618fc6a6f7
       
     1 structure ROOT = 
       
     2 struct
       
     3 
       
     4 structure Codegen = 
       
     5 struct
       
     6 
       
     7 fun double_inc a =
       
     8   IntInf.+ ((IntInf.* ((2 : IntInf.int), a)), (1 : IntInf.int));
       
     9 
       
    10 end; (*struct Codegen*)
       
    11 
       
    12 end; (*struct ROOT*)