[isabelle-dev] Exposing some functions of the API
makarius at sketis.net
Mon Oct 5 18:44:06 CEST 2015
On Thu, 1 Oct 2015, Florian Haftmann wrote:
> Is Method.rule_tac sufficient for you purpose? It is more elementary
> (and thus more predictable).
I have exported this morally public function in Isabelle/0a4c364df431. But
the purpose of all that was not explained so far.
It seems to be relevant to AFP/Isabelle_Meta_Model, but it is unclear to
me what this actually is. It contains lots of outdated / broken ML
sources from some old version of Isabelle.
More information about the isabelle-dev