Email Gateway (Aug 18 2022 at 10:21): Email Gateway (Aug 18 2022 at 10:21):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
I'm currently engaged in converting some of my Isabelle proof scripts
into Isar.
So, for example, I get
apply (tactic
"(TRYALL (dres_inst_tac [(\"x\", \"0\")] fun_cong THEN'
Force_tac))") ;
apply (tactic "(TRYALL (etac notE))") ;
apply (tactic "(TRYALL (EVERY' [ rtac ext,
dres_inst_tac [(\"x\", \"Suc ?x\")] fun_cong,
Force_tac]))") ;
Now this works, when entered during an interactive session.
It doesn't work, when it is part of a theory file.
Now this is something to do with the current theory context.
Because when I change it to
apply (tactic
"(TRYALL (dres_inst_tac [(\"x\", \"0\")] fun_cong THEN'
CLASIMPSET' force_tac))") ;
apply (tactic "(TRYALL (etac notE))") ;
apply (tactic "(TRYALL (EVERY' [ rtac ext,
dres_inst_tac [(\"x\", \"Suc ?x\")] fun_cong,
CLASIMPSET' force_tac]))") ;
it does work.
However I would very much like to know why.
Any help would be appreciated.
Jeremy
Last updated: May 03 2024 at 08:18 UTC