[isabelle-dev] Updating the current theory

Alexander Krauss krauss at in.tum.de
Sun Nov 28 10:31:13 CET 2010

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 

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 


More information about the isabelle-dev mailing list