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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
