> As far as I can tell, the result is a
> unification of two previously distinct constants, split and prod_case. I
> must confess that this duplication has never bothered me.
Just to make it clear, this distinction is extinct since approx. 2009.
What remains is a quite mechanical and
Hi Frédéric,
> During some programming tasks, I had to use the following functions:
>
> BNF_FP_Def_Sugar.co_datatype_cmd
note that these *_cmd functions are merely supposed to be used when
declaring Isar commands; dervived Isabelle/ML code is always supposed to
work with proper internalized
>> Personally I would appreciate some move here, but this only makes sense
>> if we agree what the goal is and whether it is worth the effort.
> Unless we
> can make that notation work, I don't think we profit much by a change.
> Hence I am inclined to leave things as they are.
Ditto.
Hi Florian, Frédéric,
Sorry for not answering this earlier. Somehow, I failed to notice that two of
the three functions are my responsibility.
>> During some programming tasks, I had to use the following functions:
>>
>> BNF_FP_Def_Sugar.co_datatype_cmd
>
> note that these *_cmd functions are
