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?
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
