[isabelle-dev] Exposing some functions of the API
frederic.tuong at lri.fr
Tue Oct 6 01:53:15 CEST 2015
>>> During some programming tasks, I had to use the following functions:
>> 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
> 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.
More information about the isabelle-dev