[isabelle-dev] Updating the current theory
makarius at sketis.net
Sun Nov 28 14:19:30 CET 2010
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.
More information about the isabelle-dev