Email Gateway (Aug 17 2022 at 14:15): Email Gateway (Aug 17 2022 at 14:15):From: Alexander Krauss <krauss@in.tum.de>
Ola´ Francisco, nice to hear from you again,
Isn't the SUBGOAL tactical (see reference manual) what you need?
Something like
SUBGOAL (fn (t, i)=> REPEAT_DETERM_N (complexity t) your_tactic)
should do what you need...
I leave "b)" to someone else :-)
Alex
Email Gateway (Aug 17 2022 at 14:16):From: Lawrence Paulson <lp15@cam.ac.uk>
I think you mean that you are looking for a tactic that applies the
rule repeatedly until every occurrence of xRy has been used. You'd
have to write ML code to locate them and instantiate the rule
appropriately, e.g. calling res_inst_tac, since unguided rule
applications will always find the first occurrence of xRy.
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC