[isabelle-dev] Updating the current theory

[Makarius]

On Sat, 27 Nov 2010, Michael Chan wrote:

> 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...)'.

Within a proof the background theory is strictly read-only. I don't know 
what happens if you try to change it.  Probably the system will halt and 
catch fire at some point.


 	Makarius