[isabelle-dev] Exposing some functions of the API

Frédéric Tuong frederic.tuong at lri.fr
Tue Oct 6 01:53:15 CEST 2015


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

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


More information about the isabelle-dev mailing list