[isabelle-dev] Exposing some functions of the API

Jasmin Blanchette jasmin.blanchette at inria.fr
Thu Oct 1 19:01:31 CEST 2015

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).



More information about the isabelle-dev mailing list