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
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
On 27/11/10 17:12, Alexander Krauss wrote:
Hi Michael,
I think you want to use
setup {*
ml_expression
*}
where ml_expression has type theory - theory.
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
