[isabelle-dev] Exposing some functions of the API

[Makarius]

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.


 	Makarius