equal
deleted
inserted
replaced
135 Otherwise we return: argl = argr |
135 Otherwise we return: argl = argr |
136 |
136 |
137 *) |
137 *) |
138 |
138 |
139 ML {* |
139 ML {* |
140 datatype alpha_type = AlphaGen | AlphaRes | AlphaLst; |
140 datatype alpha_mode = AlphaGen | AlphaRes | AlphaLst; |
141 *} |
141 *} |
142 |
142 |
143 ML {* |
143 ML {* |
144 fun atyp_const AlphaGen = @{const_name alpha_gen} |
144 fun atyp_const AlphaGen = @{const_name alpha_gen} |
145 | atyp_const AlphaRes = @{const_name alpha_res} |
145 | atyp_const AlphaRes = @{const_name alpha_res} |