[isabelle-dev] Exposing some functions of the API

[Jasmin Blanchette]

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 merely supposed to be used when
> declaring Isar commands; dervived Isabelle/ML code is always supposed to
> work with proper internalized entities (types term, typ, …).  The
> corresponding interface is available as BNF_FP_Def_Sugar.co_datatypes.

This is sound advice. Nonetheless, I believe I read on this mailing list that it is good practice to export the "_cmd" functions. For the BNF package, we export many but not all of them. This is now rectified (484f7878ede4).

>> Metis_Tactic.metis_method
> 
> Sounds reasonable at first sight.  What do the maintainers of metis think?

Good idea (9f9b088d8824).

Cheers,

Jasmin