[isabelle-dev] Exposing some functions of the API

[Florian Haftmann]

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

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