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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
