Hi Michael,
Thanks, Alex. Indeed, the effect I'm after is like using setup {* *}, but ultimately I'd like this effect to be produced by calling a tactic, i.e. let a tactic make updates to the current theory when invoked using 'apply (tac...)'.
AFAIK, this is impossible. Tactics/methods cannot update the theory, they just operate on goals. To change the theory you need to issue a declaration, either via "setup" or a command of your own, or by using attributes.
Don't try to use imperative things like Isar.>> and don't mess with the Toplevel. It will almost certainly break some fundamental invariants and not solve your problem. Instead, try to move the theory transformation elsewhere.
Alex _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
