[isabelle-dev] Exposing some functions of the API

[Frédéric Tuong]

Hi,

>>> 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.
I tend to use the corresponding "typed" versions of these *_cmd commands 
most of the time when possible. On the other hand, the native _cmd 
versions was also quite helpful for me to parse and implement raw Isar 
commands...


>> Classical.rule_tac
> Is Method.rule_tac sufficient for you purpose?  It is more elementary
> (and thus more predictable).
Method.rule_tac was initially used in AFP/Isabelle_Meta_Model, but I was 
surprised by its behavior when Method.rule_tac was applied with an empty 
list as parameter (then I realized that I was looking for an algorithm 
similar as Classical.rule_tac).

Thank you for your respective commits!

Whereas AFP/Isabelle_Meta_Model correctly compiles with Isabelle 2015, I 
plan to submit an updated version of the overall so that it will also 
compile with the Isabelle development version.

Cheers,
Frédéric