changeset 24249 | 1f60b45c5f97 |
parent 24221 | dd4a7ea0e64a |
child 24348 | c708ea5b109a |
24248:d276e4b53d6b | 24249:1f60b45c5f97 |
---|---|
425 [symmetric, code inline]: "arbitrary_TT = arbitrary" |
425 [symmetric, code inline]: "arbitrary_TT = arbitrary" |
426 |
426 |
427 code_datatype L0 L1 arbitrary_LT |
427 code_datatype L0 L1 arbitrary_LT |
428 code_datatype T0 T1 T2 arbitrary_TT |
428 code_datatype T0 T1 T2 arbitrary_TT |
429 |
429 |
430 code_gen higman_idx in SML to Higman |
430 code_gen higman_idx in SML module_name Higman |
431 |
431 |
432 ML {* |
432 ML {* |
433 local |
433 local |
434 open Higman |
434 open Higman |
435 in |
435 in |