[isabelle-dev] Exposing some functions of the API
florian.haftmann at informatik.tu-muenchen.de
Thu Oct 1 16:50:08 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.
Is Method.rule_tac sufficient for you purpose? It is more elementary
(and thus more predictable).
Sounds reasonable at first sight. What do the maintainers of metis think?
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 198 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev