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