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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
