[isabelle-dev] Exposing some functions of the API

Makarius makarius at sketis.net
Mon Oct 5 18:44:06 CEST 2015

On Thu, 1 Oct 2015, Florian Haftmann wrote:

>> Classical.rule_tac
> 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 mailing list