[isabelle-dev] Exposing some functions of the API

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Oct 1 16:50:08 CEST 2015

Hi Frédéric,

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

> Classical.rule_tac

Is Method.rule_tac sufficient for you purpose?  It is more elementary
(and thus more predictable).

> Metis_Tactic.metis_method

Sounds reasonable at first sight.  What do the maintainers of metis think?



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20151001/673cd807/attachment.asc>

More information about the isabelle-dev mailing list