[isabelle-dev] Updating the current theory

[Alexander Krauss]

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