doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
changeset 21172 eea3c9048c7a
parent 21147 737a94f047e3
child 21190 08ec81dfc7fb
equal deleted inserted replaced
21171:7b4fb2a2c75e 21172:eea3c9048c7a
     8 
     8 
     9 fun plus_nat (Succ_nat m) n = plus_nat m (Succ_nat n)
     9 fun plus_nat (Succ_nat m) n = plus_nat m (Succ_nat n)
    10   | plus_nat Zero_nat y = y;
    10   | plus_nat Zero_nat y = y;
    11 
    11 
    12 fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n)
    12 fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n)
    13   | times_nat Zero_nat na = Zero_nat;
    13   | times_nat Zero_nat n = Zero_nat;
    14 
    14 
    15 end; (*struct IntDef*)
    15 end; (*struct IntDef*)
    16 
    16 
    17 structure Codegen = 
    17 structure Codegen = 
    18 struct
    18 struct